# HG changeset patch
# User wenzelm
# Date 1444218834 -7200
# Node ID 1c710116b44d7825e769777a589e7f8acd3cc9a2
# Parent  c0c8bce2a21b38565ef51892ca5d626d5525970a# Parent  31829cf53f5df0581eaef710eb815e7315eb9215
merged

diff -r c0c8bce2a21b -r 1c710116b44d etc/settings
--- 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"
 
diff -r c0c8bce2a21b -r 1c710116b44d src/HOL/SPARK/Tools/spark_vcs.ML
--- 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
diff -r c0c8bce2a21b -r 1c710116b44d src/Pure/raw_simplifier.ML
--- 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 ()))
diff -r c0c8bce2a21b -r 1c710116b44d src/Tools/permanent_interpretation.ML
--- 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;