src/Tools/induct.ML
changeset 25985 8d69087f6a4b
parent 25959 9ad285dbc7a4
child 26291 d01bf7b10c75
--- a/src/Tools/induct.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/Tools/induct.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -714,7 +714,7 @@
 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
 
 val def_inst =
-  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
+  ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
       -- Args.term) >> SOME ||
     inst >> Option.map (pair NONE);