tuning

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue May 13 10:15:50 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue May 13 11:10:22 2014 +0200
@@ -1431,11 +1431,11 @@
     (goalss, after_qed, lthy')
   end;
 
-fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs') lthy =
+fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
   let
     val (raw_specs, of_specs_opt) =
-      split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy));
-    val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy;
+      split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
+    val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
   in
     add_primcorec_ursive auto opts fixes specs of_specs_opt lthy
     handle ERROR str => primcorec_error str

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue May 13 10:15:50 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue May 13 11:10:22 2014 +0200
@@ -531,12 +531,12 @@
 val add_primrec_simple = add_primrec_simple' [];
 
 fun gen_primrec old_primrec prep_spec opts
-    (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy =
+    (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy =
   let
     val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
     val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []);
 
-    val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy);
+    val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
 
     val mk_notes =
       flat ooo map3 (fn js => fn prefix => fn thms =>
@@ -558,7 +558,7 @@
       #> Local_Theory.notes (mk_notes jss names simpss)
       #>> pair ts o map snd)
   end
-  handle OLD_PRIMREC () => old_primrec raw_fixes raw_spec lthy |>> apsnd single;
+  handle OLD_PRIMREC () => old_primrec raw_fixes raw_specs lthy |>> apsnd single;
 
 val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec [];
 val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec;
@@ -581,6 +581,6 @@
   ((Scan.optional (@{keyword "("} |--
       Parse.!!! (Parse.list1 primrec_option_parser) --| @{keyword ")"}) []) --
     (Parse.fixes -- Parse_Spec.where_alt_specs)
-    >> (fn (opts, (fixes, spec)) => snd o add_primrec_cmd opts fixes spec));
+    >> (fn (opts, (fixes, specs)) => snd o add_primrec_cmd opts fixes specs));
 
 end;

--- a/src/Pure/Isar/parse_spec.ML	Tue May 13 10:15:50 2014 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Tue May 13 11:10:22 2014 +0200
@@ -158,4 +158,3 @@
 val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
 
 end;
-