# 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