From f4254821ace28d160d77178897a123adaa6f5575 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Thu, 24 Mar 2016 18:13:20 +0100
Subject: [PATCH] update to Isabelle2016
---
src/main/isabelle/stateful_ops.ML | 4 ++--
src/main/isabelle/tactics.ML | 9 ++++-----
src/main/isabelle/util.ML | 4 ++--
src/main/scala/leon/solvers/isabelle/package.scala | 2 +-
4 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/src/main/isabelle/stateful_ops.ML b/src/main/isabelle/stateful_ops.ML
index 2289e3e6e..18f0d6400 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 639c1348b..d2a5ce83b 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/util.ML b/src/main/isabelle/util.ML
index 2401cfb4b..55be31d11 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 c06f4f59b..2e5341013 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 {
--
GitLab