src/HOL/Tools/BNF/bnf_lfp.ML
changeset 56344 1014f44c62a2
parent 56272 159c07ceb18c
child 56346 42533f8f4729
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 31 21:15:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Apr 01 10:04:05 2014 +0200
@@ -787,11 +787,7 @@
 
     val car_inits = map (mk_min_alg str_inits) ks;
 
-    (*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
-    val alg_init_thm = Goal.prove_sorry lthy [] []
-      (HOLogic.mk_Trueprop (mk_alg car_inits str_inits))
-      (K (rtac alg_min_alg_thm 1))
-      |> Thm.close_derivation;
+    val alg_init_thm = cterm_instantiate_pos (map (SOME o certify lthy) str_inits) alg_min_alg_thm;
 
     val alg_select_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_Ball II