--- a/etc/settings Wed Oct 07 13:34:42 2015 +0200
+++ b/etc/settings Wed Oct 07 13:53:54 2015 +0200
@@ -14,7 +14,7 @@
ISABELLE_SCALA_BUILD_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.7 -Xmax-classfile-name 130"
-ISABELLE_JAVA_SYSTEM_OPTIONS="-server -XX:+UseG1GC -XX:+UseStringDeduplication -Dfile.encoding=UTF-8 -Disabelle.threads=0"
+ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Oct 07 13:34:42 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Wed Oct 07 13:53:54 2015 +0200
@@ -1010,27 +1010,27 @@
fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
(case lookup consts s of
- SOME ty =>
- let
- val (t, ty') = term_of_expr thy prfx types pfuns ids e;
- val T = mk_type thy prfx ty;
- val T' = mk_type thy prfx ty';
- val _ = T = T' orelse
- error ("Declared type " ^ ty ^ " of " ^ s ^
- "\ndoes not match type " ^ ty' ^ " in definition");
- val id' = mk_rulename id;
- val lthy = Named_Target.theory_init thy;
- val ((t', (_, th)), lthy') = Specification.definition
- (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Free (s, T), t)))) lthy;
- val phi = Proof_Context.export_morphism lthy' lthy
- in
- ((id', Morphism.thm phi th),
- ((Symtab.update (s, (Morphism.term phi t', ty)) tab,
- Name.declare s ctxt),
- Local_Theory.exit_global lthy'))
+ SOME ty =>
+ let
+ val (t, ty') = term_of_expr thy prfx types pfuns ids e;
+ val T = mk_type thy prfx ty;
+ val T' = mk_type thy prfx ty';
+ val _ = T = T' orelse
+ error ("Declared type " ^ ty ^ " of " ^ s ^
+ "\ndoes not match type " ^ ty' ^ " in definition");
+ val id' = mk_rulename id;
+ val ((t', (_, th)), lthy') = Named_Target.theory_init thy
+ |> Specification.definition
+ (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t))));
+ val phi =
+ Proof_Context.export_morphism lthy'
+ (Proof_Context.init_global (Proof_Context.theory_of lthy'));
+ in
+ ((id', Morphism.thm phi th),
+ ((Symtab.update (s, (Morphism.term phi t', ty)) tab, Name.declare s ctxt),
+ Local_Theory.exit_global lthy'))
end
- | NONE => error ("Undeclared constant " ^ s));
+ | NONE => error ("Undeclared constant " ^ s));
fun add_var prfx (s, ty) (ids, thy) =
let val ([Free p], ids') = mk_variables thy prfx [s] ty ids
--- a/src/Pure/raw_simplifier.ML Wed Oct 07 13:34:42 2015 +0200
+++ b/src/Pure/raw_simplifier.ML Wed Oct 07 13:53:54 2015 +0200
@@ -1381,13 +1381,15 @@
local
-fun gen_norm_hhf ss ctxt th =
- (if Drule.is_norm_hhf (Thm.prop_of th) then th
- else
- Conv.fconv_rule
- (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
- |> Thm.adjust_maxidx_thm ~1
- |> Variable.gen_all ctxt;
+fun gen_norm_hhf ss ctxt =
+ Thm.transfer (Proof_Context.theory_of ctxt) #>
+ (fn th =>
+ if Drule.is_norm_hhf (Thm.prop_of th) then th
+ else
+ Conv.fconv_rule
+ (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th) #>
+ Thm.adjust_maxidx_thm ~1 #>
+ Variable.gen_all ctxt;
val hhf_ss =
simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
--- a/src/Tools/permanent_interpretation.ML Wed Oct 07 13:34:42 2015 +0200
+++ b/src/Tools/permanent_interpretation.ML Wed Oct 07 13:53:54 2015 +0200
@@ -34,8 +34,10 @@
val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
- val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt1) o snd o snd) defs;
val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
+ val def_eqns = defs
+ |> map (Thm.symmetric o
+ Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt2) o snd o snd);
(*setting up*)
val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;