--- a/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 04 21:42:40 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 04 22:30:12 2014 +0100
@@ -195,11 +195,11 @@
fun mk_simplified_set set =
let
val setT = fastype_of set;
- val schem_set' = Const (@{const_name id_bnf_comp}, setT --> setT) $ Var (("?x", 0), setT);
- val goal = mk_Trueprop_eq (schem_set', set);
+ val var_set' = Const (@{const_name id_bnf_comp}, setT --> setT) $ Var ((Name.uu, 0), setT);
+ val goal = mk_Trueprop_eq (var_set', set);
fun tac {context = ctxt, prems = _} = mk_simplified_set_tac ctxt;
val set'_eq_set =
- Goal.prove_sorry names_lthy [] [] goal tac
+ Goal.prove names_lthy [] [] goal tac
|> Thm.close_derivation;
val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set)));
in