1.1 --- a/src/Tools/Code/code_thingol.ML	Thu Apr 19 09:45:49 2012 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Apr 19 09:58:54 2012 +0200
     1.3 @@ -270,7 +270,6 @@
     1.4  local
     1.5    fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
     1.6    fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
     1.7 -  fun thyname_of_const' thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
     1.8    fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
     1.9     of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
    1.10      | thyname :: _ => thyname;
    1.11 @@ -278,7 +277,7 @@
    1.12     of SOME class => thyname_of_class thy class
    1.13      | NONE => (case Code.get_type_of_constr_or_abstr thy c
    1.14         of SOME (tyco, _) => thyname_of_type thy tyco
    1.15 -        | NONE => thyname_of_const' thy c);
    1.16 +        | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
    1.17    fun purify_base "==>" = "follows"
    1.18      | purify_base "==" = "meta_eq"
    1.19      | purify_base s = Name.desymbolize false s;
    1.20 @@ -471,11 +470,6 @@
    1.21  fun is_case (Fun (_, (_, SOME _))) = true
    1.22    | is_case _ = false;
    1.23  
    1.24 -fun lookup_classparam_instance program name = program |> Graph.get_first
    1.25 -  (fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) =>
    1.26 -    Option.map (fn ((const, _), _) => (class, const))
    1.27 -      (find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE)
    1.28 -  
    1.29  fun labelled_name thy program name =
    1.30    let val ctxt = Proof_Context.init_global thy in
    1.31      case Graph.get_node program name of