1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue May 13 10:15:50 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue May 13 11:10:22 2014 +0200
     1.3 @@ -1431,11 +1431,11 @@
     1.4      (goalss, after_qed, lthy')
     1.5    end;
     1.6  
     1.7 -fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs') lthy =
     1.8 +fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
     1.9    let
    1.10      val (raw_specs, of_specs_opt) =
    1.11 -      split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy));
    1.12 -    val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy;
    1.13 +      split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
    1.14 +    val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
    1.15    in
    1.16      add_primcorec_ursive auto opts fixes specs of_specs_opt lthy
    1.17      handle ERROR str => primcorec_error str

     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue May 13 10:15:50 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue May 13 11:10:22 2014 +0200
     2.3 @@ -531,12 +531,12 @@
     2.4  val add_primrec_simple = add_primrec_simple' [];
     2.5  
     2.6  fun gen_primrec old_primrec prep_spec opts
     2.7 -    (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy =
     2.8 +    (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy =
     2.9    let
    2.10      val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
    2.11      val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []);
    2.12  
    2.13 -    val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy);
    2.14 +    val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
    2.15  
    2.16      val mk_notes =
    2.17        flat ooo map3 (fn js => fn prefix => fn thms =>
    2.18 @@ -558,7 +558,7 @@
    2.19        #> Local_Theory.notes (mk_notes jss names simpss)
    2.20        #>> pair ts o map snd)
    2.21    end
    2.22 -  handle OLD_PRIMREC () => old_primrec raw_fixes raw_spec lthy |>> apsnd single;
    2.23 +  handle OLD_PRIMREC () => old_primrec raw_fixes raw_specs lthy |>> apsnd single;
    2.24  
    2.25  val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec [];
    2.26  val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec;
    2.27 @@ -581,6 +581,6 @@
    2.28    ((Scan.optional (@{keyword "("} |--
    2.29        Parse.!!! (Parse.list1 primrec_option_parser) --| @{keyword ")"}) []) --
    2.30      (Parse.fixes -- Parse_Spec.where_alt_specs)
    2.31 -    >> (fn (opts, (fixes, spec)) => snd o add_primrec_cmd opts fixes spec));
    2.32 +    >> (fn (opts, (fixes, specs)) => snd o add_primrec_cmd opts fixes specs));
    2.33  
    2.34  end;

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