# HG changeset patch
# User traytel
# Date 1396339445 -7200
# Node ID 1014f44c62a2fcccdf6f0be4ad8cd864bf4dabed
# Parent  97d6a786e0f9c6299a20dcced580190903f18a54
tuned

diff -r 97d6a786e0f9 -r 1014f44c62a2 src/HOL/Tools/BNF/bnf_lfp.ML
--- 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