Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authortraytel
Tue, 01 Apr 2014 10:04:05 +0200
changeset 56344 1014f44c62a2
parent 56343 97d6a786e0f9
child 56345 228e30cb111d
tuned
src/HOL/Tools/BNF/bnf_lfp.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle