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_package.ML
changeset 24589 d3fca349736c
parent 24423 ae9cd0e92423
child 24624 b8383b1bbae3 
--- a/src/HOL/Tools/datatype_package.ML	Sat Sep 15 19:27:43 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sat Sep 15 19:27:44 2007 +0200
@@ -565,7 +565,7 @@
         val n = Sign.arity_number thy tyco;
       in
         thy
-        |> Class.prove_instance_arity (Class.intro_classes_tac [])
+        |> Class.prove_instance (Class.intro_classes_tac [])
             [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
         |> snd
       end
isabelle