author wenzelm Sun, 23 Mar 2014 15:46:21 +0100 changeset 56259 0d301d91444b parent 56258 fec233e7f67d child 56260 3d79c132e657
more sensible treatment of quasi-local variables (NB: Variable.add_fixes is only for term variables, while Variable.declare takes care of types within given terms);
```--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 22:00:26 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun Mar 23 15:46:21 2014 +0100
@@ -944,17 +944,17 @@
let
val th = case_rewrite thy Tcon
val ctxt = Proof_Context.init_global thy
-    val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
+    val f = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
-    val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
-    val T' = TFree (tname', @{sort type})
-    val U = TFree (uname, @{sort type})
+    val ([yname], ctxt') = Variable.add_fixes ["y"] ctxt
+    val T' = TFree ("'t'", @{sort type})
+    val U = TFree ("'u", @{sort type})
val y = Free (yname, U)
val f' = absdummy (U --> T') (Bound 0 \$ y)
val th' = Thm.certify_instantiate
([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
[((fst (dest_Var f), (U --> T') --> T'), f')]) th
-    val [th'] = Variable.export ctxt' ctxt [th']
+    val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
in
th'
end```