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/Tools/Datatype/datatype_codegen.ML
changeset 38348 cf7b2121ad9d
parent 37425 b5492f611129
child 38538 c87b69396a37 
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -115,7 +115,7 @@
       #> snd
   in
     thy
-    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
+    |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
     |> fold_map add_def dtcos
     |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
          (fn _ => fn def_thms => tac def_thms) def_thms)
isabelle