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/datatype.ML
changeset 1810 0eef167ebe1b
parent 1690 e0ff33a33fa5
child 1897 71e51870cc9a 
--- a/src/HOL/datatype.ML	Mon Jun 17 16:51:47 1996 +0200
+++ b/src/HOL/datatype.ML	Tue Jun 18 16:17:38 1996 +0200
@@ -224,8 +224,8 @@
       
       val xrules =
         let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
-        in [("logic", "case x of " ^ first_part) <->
-             ("logic", tname ^ "_case " ^ scnd_part ^ " x")]
+        in [Syntax.<-> (("logic", "case x of " ^ first_part),
+			("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
         end;
 
      (*type declarations for constructors*)
isabelle