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/Provers/induct_method.ML
changeset 24022 ab76c73b3b58
parent 23591 d32a85385e17 
--- 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 ||
isabelle