src/HOL/Tools/recdef.ML
changeset 47815 43f677b3ae91
parent 47067 4ef29b0c568f
child 50214 67fb9a168d10
     1.1 --- a/src/HOL/Tools/recdef.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/HOL/Tools/recdef.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4        |> Sign.parent_path;
     1.5    in (thy, result) end;
     1.6  
     1.7 -val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
     1.8 +val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global prepare_hints;
     1.9  fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
    1.10  
    1.11