1.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -268,8 +268,8 @@
     1.4        error ("No termination condition #" ^ string_of_int i ^
     1.5          " in recdef definition of " ^ quote name);
     1.6    in
     1.7 -    Specification.theorem Thm.internalK NONE (K I) (bname, atts)
     1.8 -      [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
     1.9 +    Specification.theorem Thm.internalK NONE (K I) (Name.binding bname, atts)
    1.10 +      [] (Element.Shows [((Name.no_binding, []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    1.11    end;
    1.12  
    1.13  val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
    1.14 @@ -299,7 +299,8 @@
    1.15  
    1.16  val recdef_decl =
    1.17    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
    1.18 -  P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
    1.19 +  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
    1.20 +    -- Scan.option hints
    1.21    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
    1.22  
    1.23  val _ =
    1.24 @@ -319,7 +320,8 @@
    1.25  val _ =
    1.26    OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
    1.27      K.thy_goal
    1.28 -    (SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    1.29 +    ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
    1.30 +        Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    1.31        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
    1.32  
    1.33  end;