1.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -299,7 +299,7 @@
     1.4  
     1.5  val recdef_decl =
     1.6    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
     1.7 -  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
     1.8 +  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
     1.9      -- Scan.option hints
    1.10    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
    1.11  
    1.12 @@ -320,7 +320,7 @@
    1.13  val _ =
    1.14    OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
    1.15      K.thy_goal
    1.16 -    ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
    1.17 +    ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname --
    1.18          Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    1.19        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
    1.20