diff -r 491c68f40bc4 -r ab76c73b3b58 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Sat Jul 28 20:40:26 2007 +0200
+++ b/src/Provers/induct_method.ML	Sat Jul 28 20:40:27 2007 +0200
@@ -476,10 +476,10 @@
   | single_rule _ = error "Single rule expected";
 
 fun named_rule k arg get =
-  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :--
+  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
     (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
       (case get (Context.proof_of context) name of SOME x => x
-      | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2;
+      | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_set =
   named_rule InductAttrib.typeN Args.tyname get_type ||