src/Tools/induct.ML

 val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule;
 
 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);
 
 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
   error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of context) t));