| 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);