src/Tools/Code/code_thingol.ML
changeset 42359 6ca5407863ed
parent 42284 326f57825e1a
child 42361 23f352990944
     1.1 --- a/src/Tools/Code/code_thingol.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -489,20 +489,29 @@
     1.4        end
     1.5    | _ => [];
     1.6  
     1.7 -fun labelled_name thy program name = case Graph.get_node program name
     1.8 - of Fun (c, _) => quote (Code.string_of_const thy c)
     1.9 -  | Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
    1.10 -  | Datatypecons (c, _) => quote (Code.string_of_const thy c)
    1.11 -  | Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
    1.12 -  | Classrel (sub, super) => let
    1.13 -        val Class (sub, _) = Graph.get_node program sub
    1.14 -        val Class (super, _) = Graph.get_node program super
    1.15 -      in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
    1.16 -  | Classparam (c, _) => quote (Code.string_of_const thy c)
    1.17 -  | Classinst ((class, (tyco, _)), _) => let
    1.18 -        val Class (class, _) = Graph.get_node program class
    1.19 -        val Datatype (tyco, _) = Graph.get_node program tyco
    1.20 -      in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
    1.21 +fun labelled_name thy program name =
    1.22 +  let val ctxt = ProofContext.init_global thy in
    1.23 +    case Graph.get_node program name of
    1.24 +      Fun (c, _) => quote (Code.string_of_const thy c)
    1.25 +    | Datatype (tyco, _) => "type " ^ quote (ProofContext.extern_type ctxt tyco)
    1.26 +    | Datatypecons (c, _) => quote (Code.string_of_const thy c)
    1.27 +    | Class (class, _) => "class " ^ quote (ProofContext.extern_class ctxt class)
    1.28 +    | Classrel (sub, super) =>
    1.29 +        let
    1.30 +          val Class (sub, _) = Graph.get_node program sub;
    1.31 +          val Class (super, _) = Graph.get_node program super;
    1.32 +        in
    1.33 +          quote (ProofContext.extern_class ctxt sub ^ " < " ^ ProofContext.extern_class ctxt super)
    1.34 +        end
    1.35 +    | Classparam (c, _) => quote (Code.string_of_const thy c)
    1.36 +    | Classinst ((class, (tyco, _)), _) =>
    1.37 +        let
    1.38 +          val Class (class, _) = Graph.get_node program class;
    1.39 +          val Datatype (tyco, _) = Graph.get_node program tyco;
    1.40 +        in
    1.41 +          quote (ProofContext.extern_type ctxt tyco ^ " :: " ^ ProofContext.extern_class ctxt class)
    1.42 +        end
    1.43 +  end;
    1.44  
    1.45  fun linear_stmts program =
    1.46    rev (Graph.strong_conn program)