# HG changeset patch
# User blanchet
# Date 1393968612 -3600
# Node ID e6d570cb0f5ef89f4c24ca1e533a7151fb0eff23
# Parent  685256e78dd80673f64cd814f8fd033e5cab896b
no 'sorry' so that the schematic variable gets instantiated

diff -r 685256e78dd8 -r e6d570cb0f5e src/HOL/Tools/BNF/bnf_comp.ML
--- 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