# HG changeset patch
# User wenzelm
# Date 1441040367 -7200
# Node ID 1727d7d14d76928ba8c809a966c5ebf89ed6a552
# Parent  b7e82288353586a9e4e391006cf0c8b22386fa81
routine check of theory context;

diff -r b7e822883535 -r 1727d7d14d76 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Oct 06 21:12:01 2015 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon Aug 31 18:59:27 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 ()))