src/Tools/Code/code_printer.ML
changeset 32924 d2e9b2dab760
parent 32913 3e9809678574
child 33955 fff6f11b1f09
child 33989 cb136b5f6050
     1.1 --- a/src/Tools/Code/code_printer.ML	Tue Oct 13 14:57:53 2009 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Wed Oct 14 11:56:44 2009 +0200
     1.3 @@ -316,13 +316,13 @@
     1.4  val dest_name =
     1.5    apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
     1.6  
     1.7 -fun mk_name_module reserved_names module_prefix module_alias program =
     1.8 +fun mk_name_module reserved module_prefix module_alias program =
     1.9    let
    1.10      fun mk_alias name = case module_alias name
    1.11       of SOME name' => name'
    1.12        | NONE => name
    1.13            |> Long_Name.explode
    1.14 -          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
    1.15 +          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
    1.16            |> Long_Name.implode;
    1.17      fun mk_prefix name = case module_prefix
    1.18       of SOME module_prefix => Long_Name.append module_prefix name