diff --git a/src/main/isabelle/stateful_ops.ML b/src/main/isabelle/stateful_ops.ML
index 2289e3e6e6311b9fa35d819db29794b433c897a9..18f0d6400b16879fb6b9d68433d0099eb52bb0eb 100644
--- a/src/main/isabelle/stateful_ops.ML
+++ b/src/main/isabelle/stateful_ops.ML
@@ -486,10 +486,10 @@ fun lookup_datatype (name, raw_constructors) =
(Codec.Left ("unknown datatype " ^ name), lthy)
| SOME {ctrs, discs, selss, split, split_asm, case_thms, ...} =>
let
- val raw_constructors = sort_wrt snd (raw_constructors)
+ val raw_constructors = sort_by snd (raw_constructors)
val (names, terms) =
map (fst o dest_Const) ctrs ~~ (discs ~~ selss)
- |> sort_wrt fst
+ |> sort_by fst
|> split_list
fun process (internal_name, name) (disc, sels) =
(internal_name, (Const (name, dummyT), dummify_types disc, map dummify_types sels))
diff --git a/src/main/isabelle/tactics.ML b/src/main/isabelle/tactics.ML
index 639c1348b43666f15ee9d5dca347ddd16b6f5a77..d2a5ce83b8499bcc45bd0037a992e56f9f7d30c7 100644
--- a/src/main/isabelle/tactics.ML
+++ b/src/main/isabelle/tactics.ML
@@ -31,8 +31,8 @@ fun equiv_tac rule ctxt =
|> Syntax.check_term ctxt
|> Thm.cterm_of ctxt
- val insts = [(Thm.cterm_of ctxt p, p_inst)]
- val rule = Drule.cterm_instantiate insts rule
+ val insts = [(fst (dest_Var p), p_inst)]
+ val rule = Drule.infer_instantiate ctxt insts rule
in ext_tac (length args) n THEN resolve_tac ctxt [rule] n end)
val maybe_induct =
@@ -53,8 +53,7 @@ fun method_tac pos src = Subgoal.FOCUS (fn {context = ctxt, concl, ...} =>
|> Scan.catch scan
val state =
Proof.theorem NONE (K I) [[(Thm.term_of concl, [])]] ctxt
- |> Proof.refine m
- |> Seq.hd
+ |> Proof.refine_singleton m
val {goal, ...} = Proof.simple_goal state
in
HEADGOAL (resolve_tac ctxt [Goal.conclude goal])
@@ -64,4 +63,4 @@ fun pat_completeness_auto_tac ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
fun termination_tac ctxt =
- Function_Common.termination_prover_tac ctxt
\ No newline at end of file
+ Function_Common.termination_prover_tac true ctxt
\ No newline at end of file
diff --git a/src/main/isabelle/term_codec.ML b/src/main/isabelle/term_codec.ML
deleted file mode 100644
index be8e81e96bf557dbfe8cb1e4f4a221b308f9b494..0000000000000000000000000000000000000000
--- a/src/main/isabelle/term_codec.ML
+++ /dev/null
@@ -1,75 +0,0 @@
-datatype ('a, 'b) either = Left of 'a | Right of 'b
-
-structure Codec = struct
-
-open Codec
-
-fun triple a b c =
- tuple a (tuple b c)
- |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
-
-fun either a b =
- let
- fun enc (Left l) = (0, encode a l)
- | enc (Right r) = (1, encode b r)
- fun dec 0 = SOME (decode a #> map_result Left)
- | dec 1 = SOME (decode b #> map_result Right)
- | dec _ = NONE
- in Codec.variant enc dec "either" end
-
-end
-
-signature TERM_CODEC = sig
- val typ : typ codec
- val term : term codec
-end
-
-structure Term_Codec : TERM_CODEC = struct
-
-val sort : sort codec = Codec.list Codec.string
-val indexname : indexname codec = Codec.tuple Codec.string Codec.int
-
-fun typ () =
- let
- fun typ_type () = Codec.tuple Codec.string (Codec.list (typ ()))
- val typ_tfree = Codec.tuple Codec.string sort
- val typ_tvar = Codec.tuple indexname sort
-
- fun enc (Type arg) = (0, Codec.encode (typ_type ()) arg)
- | enc (TFree arg) = (1, Codec.encode typ_tfree arg)
- | enc (TVar arg) = (2, Codec.encode typ_tvar arg)
- fun dec 0 = SOME (Codec.decode (typ_type ()) #> Codec.map_result Type)
- | dec 1 = SOME (Codec.decode typ_tfree #> Codec.map_result TFree)
- | dec 2 = SOME (Codec.decode typ_tvar #> Codec.map_result TVar)
- | dec _ = NONE
- in Codec.variant enc dec "Pure.typ" end
-
-val typ = typ ()
-
-fun term () =
- let
- val term_const = Codec.tuple Codec.string typ
- val term_free = Codec.tuple Codec.string typ
- val term_var = Codec.tuple indexname typ
- val term_bound = Codec.int
- fun term_abs () = Codec.triple Codec.string typ (term ())
- fun term_app () = Codec.tuple (term ()) (term ())
-
- fun enc (Const arg) = (0, Codec.encode term_const arg)
- | enc (Free arg) = (1, Codec.encode term_free arg)
- | enc (Var arg) = (2, Codec.encode term_var arg)
- | enc (Bound arg) = (3, Codec.encode term_bound arg)
- | enc (Abs arg) = (4, Codec.encode (term_abs ()) arg)
- | enc (op $ arg) = (5, Codec.encode (term_app ()) arg)
- fun dec 0 = SOME (Codec.decode term_const #> Codec.map_result Const)
- | dec 1 = SOME (Codec.decode term_free #> Codec.map_result Free)
- | dec 2 = SOME (Codec.decode term_var #> Codec.map_result Var)
- | dec 3 = SOME (Codec.decode term_bound #> Codec.map_result Bound)
- | dec 4 = SOME (Codec.decode (term_abs ()) #> Codec.map_result Abs)
- | dec 5 = SOME (Codec.decode (term_app ()) #> Codec.map_result op $)
- | dec _ = NONE
- in Codec.variant enc dec "Pure.term" end
-
-val term = term ()
-
-end
\ No newline at end of file
diff --git a/src/main/isabelle/util.ML b/src/main/isabelle/util.ML
index 2401cfb4bd8bcacc8120b11e71e5989f244b7e3e..55be31d116b0e3be15c4ffb19b30b38946213996 100644
--- a/src/main/isabelle/util.ML
+++ b/src/main/isabelle/util.ML
@@ -117,7 +117,7 @@ fun fold_opt _ [] y = SOME y
| fold_opt f (x :: xs) y = Option.mapPartial (fold_opt f xs) (f x y)
fun fold_res _ [] y = Exn.Res y
- | fold_res f (x :: xs) y = Exn.maps_result (fold_res f xs) (f x y)
+ | fold_res f (x :: xs) y = Exn.maps_res (fold_res f xs) (f x y)
fun map_generalized f t =
case t of
@@ -229,7 +229,7 @@ fun homogenize_spec_types ctxt thms =
val typ = Sign.the_const_type (Proof_Context.theory_of ctxt) head
fun mk_subst (iname, (sort, inst)) =
- (Thm.ctyp_of ctxt (TVar (iname, sort)), Thm.ctyp_of ctxt inst)
+ ((iname, sort), Thm.ctyp_of ctxt inst)
fun instantiate ((_, ttyp), thm) =
let
diff --git a/src/main/scala/leon/solvers/isabelle/package.scala b/src/main/scala/leon/solvers/isabelle/package.scala
index c06f4f59b9f1d3eb11bf924d1812c8eb1e30dc8b..2e5341013311cd469c4fb9f1a8d3dabc10ac738d 100644
--- a/src/main/scala/leon/solvers/isabelle/package.scala
+++ b/src/main/scala/leon/solvers/isabelle/package.scala
@@ -22,7 +22,7 @@ import shapeless.tag
object `package` {
val theory = "Leon_Runtime"
- val isabelleVersion = "2015"
+ val isabelleVersion = "2016"
implicit class FutureResultOps[A](val future: Future[ProverResult[A]]) extends AnyVal {