1.1 --- a/src/Tools/Code/code_target.ML	Fri Oct 01 11:46:09 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Fri Oct 01 11:46:09 2010 +0200
     1.3 @@ -244,12 +244,10 @@
     1.4  
     1.5  fun the_literals thy = #literals o the_fundamental thy;
     1.6  
     1.7 -local
     1.8 -
     1.9 -fun activate_target thy target =
    1.10 +fun collapse_hierarchy thy =
    1.11    let
    1.12 -    val ((targets, abortable), default_width) = Targets.get thy;
    1.13 -    fun collapse_hierarchy target =
    1.14 +    val ((targets, _), _) = Targets.get thy;
    1.15 +    fun collapse target = 
    1.16        let
    1.17          val data = case Symtab.lookup targets target
    1.18           of SOME data => data
    1.19 @@ -257,10 +255,17 @@
    1.20        in case the_description data
    1.21         of Fundamental _ => (K I, data)
    1.22          | Extension (super, modify) => let
    1.23 -            val (modify', data') = collapse_hierarchy super
    1.24 +            val (modify', data') = collapse super
    1.25            in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
    1.26        end;
    1.27 -    val (modify, data) = collapse_hierarchy target;
    1.28 +  in collapse end;
    1.29 +
    1.30 +local
    1.31 +
    1.32 +fun activate_target thy target =
    1.33 +  let
    1.34 +    val ((targets, abortable), default_width) = Targets.get thy;
    1.35 +    val (modify, data) = collapse_hierarchy thy target;
    1.36    in (default_width, abortable, data, modify) end;
    1.37  
    1.38  fun activate_syntax lookup_name src_tab = Symtab.empty
    1.39 @@ -537,12 +542,16 @@
    1.40        then error ("Too many arguments in syntax for constant " ^ quote c)
    1.41        else syn);
    1.42  
    1.43 -fun add_reserved target =
    1.44 +fun add_reserved target sym thy =
    1.45    let
    1.46 -    fun add sym syms = if member (op =) syms sym
    1.47 +    val (_, data) = collapse_hierarchy thy target;
    1.48 +    val _ = if member (op =) (the_reserved data) sym
    1.49        then error ("Reserved symbol " ^ quote sym ^ " already declared")
    1.50 -      else insert (op =) sym syms
    1.51 -  in map_reserved target o add end;
    1.52 +      else ();
    1.53 +  in
    1.54 +    thy
    1.55 +    |> map_reserved target (insert (op =) sym)
    1.56 +  end;
    1.57  
    1.58  fun gen_add_include read_const target args thy =
    1.59    let