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/function_package/inductive_wrap.ML
changeset 24746 6d42be359d57
parent 22619 166b4c3b41c0
child 24816 2d0fa8f31804 
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Sep 28 10:30:51 2007 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Sep 28 10:32:38 2007 +0200
@@ -45,7 +45,7 @@
                                            false (* no coind *)
                                            false (* elims, please *)
                                            false (* induction thm please *)
-                                           [(R, SOME T, NoSyn)] (* the relation *)
+                                           [((R, T), NoSyn)] (* the relation *)
                                            [] (* no parameters *)
                                            (map (fn t => (("", []), t)) defs) (* the intros *)
                                            [] (* no special monos *)
isabelle