--- 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