src/Tools/Code/code_target.ML
changeset 32894 cdd7800de437
parent 32740 9dd0a2f83429
child 32966 5b21661fe618
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Oct 08 15:59:16 2009 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Oct 08 15:59:16 2009 +0200
     1.3 @@ -386,21 +386,6 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun labelled_name thy program name = case Graph.get_node program name
     1.8 - of Code_Thingol.Fun (c, _) => quote (Code.string_of_const thy c)
     1.9 -  | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
    1.10 -  | Code_Thingol.Datatypecons (c, _) => quote (Code.string_of_const thy c)
    1.11 -  | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
    1.12 -  | Code_Thingol.Classrel (sub, super) => let
    1.13 -        val Code_Thingol.Class (sub, _) = Graph.get_node program sub
    1.14 -        val Code_Thingol.Class (super, _) = Graph.get_node program super
    1.15 -      in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
    1.16 -  | Code_Thingol.Classparam (c, _) => quote (Code.string_of_const thy c)
    1.17 -  | Code_Thingol.Classinst ((class, (tyco, _)), _) => let
    1.18 -        val Code_Thingol.Class (class, _) = Graph.get_node program class
    1.19 -        val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
    1.20 -      in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
    1.21 -
    1.22  fun activate_syntax lookup_name src_tab = Symtab.empty
    1.23    |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
    1.24         of SOME name => (SOME name,
    1.25 @@ -440,7 +425,7 @@
    1.26      val _ = if null empty_funs then () else error ("No code equations for "
    1.27        ^ commas (map (Sign.extern_const thy) empty_funs));
    1.28    in
    1.29 -    serializer module args (labelled_name thy program2) reserved includes
    1.30 +    serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
    1.31        (Symtab.lookup module_alias) (Symtab.lookup class')
    1.32        (Symtab.lookup tyco') (Symtab.lookup const')
    1.33        program4 names2