Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Eval.thy
changeset 24626 85eceef2edc7
parent 24621 97d403d9ab54
child 24659 6b7ac2a43df8 
--- a/src/HOL/Library/Eval.thy	Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Tue Sep 18 07:46:00 2007 +0200
@@ -56,7 +56,7 @@
     DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
       [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
-in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
+in DatatypeCodegen.add_codetypes_hook hook end
 *}
 
 
@@ -118,7 +118,7 @@
       DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
       [TermOf.class_term_of] ((K o K o pair) []) mk
-in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
+in DatatypeCodegen.add_codetypes_hook hook end
 *}
 
 abbreviation
isabelle