# HG changeset patch
# User bulwahn
# Date 1352372387 -3600
# Node ID d9871e5ea0e1ec4c72c7d6c8d40c9532c218c97f
# Parent  19965e6a705e26bb8462809e5a1b45aab54cb543
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc

diff -r 19965e6a705e -r d9871e5ea0e1 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 11:59:47 2012 +0100
@@ -478,18 +478,21 @@
 fun conv ss t =
   let
     val ctxt = Simplifier.the_context ss
-    val ct = cterm_of (Proof_Context.theory_of ctxt) t
+    val ([t'], ctxt') = Variable.import_terms true [t] (Variable.declare_term t ctxt)
+    val ss' = Simplifier.context ctxt' ss
+    val ct = cterm_of (Proof_Context.theory_of ctxt') t'
     fun unfold_conv thms =
       Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
-        (Raw_Simplifier.inherit_context ss empty_ss addsimps thms)
-    val prep_eq = (comprehension_conv ss then_conv unfold_conv prep_thms) ct
-    val t' = term_of (Thm.rhs_of prep_eq)
-    fun mk_thm (fm, t'') = Goal.prove ctxt [] []
-      (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1)
+        (Raw_Simplifier.inherit_context ss' empty_ss addsimps thms)
+    val prep_eq = (comprehension_conv ss' then_conv unfold_conv prep_thms) ct
+    val t'' = term_of (Thm.rhs_of prep_eq)
+    fun mk_thm (fm, t''') = Goal.prove ctxt' [] []
+      (HOLogic.mk_Trueprop (HOLogic.mk_eq (t'', t'''))) (fn {context, ...} => tac context fm 1)
     fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans})
     val post = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
+    val export = singleton (Variable.export ctxt' ctxt)
   in
-    Option.map (post o unfold o mk_thm) (rewrite_term t')
+    Option.map (export o post o unfold o mk_thm) (rewrite_term t'')
   end;
 
 fun base_simproc ss redex =