# HG changeset patch
# User wenzelm
# Date 1146850355 -7200
# Node ID 0d673faf560c8ee14f020d012494d7f78e3d2fcf
# Parent  f199cb2295fd00be601271f07f608494249033e1
Theory.definitions_of;

diff -r f199cb2295fd -r 0d673faf560c src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri May 05 19:32:34 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Fri May 05 19:32:35 2006 +0200
@@ -127,9 +127,9 @@
 
 type deftab = (typ * thm) list Symtab.table;
 
-fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c
- of [] => true
-  | [(ty, _)] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
+fun is_overloaded thy c = case Theory.definitions_of thy c
+ of [] => true   (* FIXME false (!?) *)
+  | [{lhs = ty, ...}] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
   | _ => true;
 
 structure InstNameMangler = NameManglerFun (
@@ -152,9 +152,9 @@
     let
       val c' = idf_of_name thy nsp_overl c;
       val prefix = 
-        case (AList.lookup (Sign.typ_equiv thy)
-            (Defs.specifications_of (Theory.defs_of thy) c)) ty
-         of SOME (_, thyname) => NameSpace.append thyname nsp_overl
+        case (find_first (fn {lhs, ...} => Sign.typ_equiv thy (ty, lhs))
+            (Theory.definitions_of thy c))
+         of SOME {module, ...} => NameSpace.append module nsp_overl
           | NONE => if c = "op ="
               then
                 NameSpace.append
@@ -930,17 +930,17 @@
       |> Symtab.fold
           (fn (c, _) =>
             let
-              val deftab = Defs.specifications_of (Theory.defs_of thy) c
+              val deftab = Theory.definitions_of thy c
               val is_overl = (is_none o ClassPackage.lookup_const_class thy) c
-               andalso case deftab
+               andalso case deftab   (* is_overloaded (!?) *)
                of [] => false
-                | [(ty, _)] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
+                | [{lhs = ty, ...}] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
                 | _ => true;
             in if is_overl then (fn (overltab1, overltab2) => (
               overltab1
-              |> Symtab.update_new (c, map fst deftab),
+              |> Symtab.update_new (c, map #lhs deftab),
               overltab2
-              |> fold_map (fn (ty, _) => ConstNameMangler.declare thy (c, ty)) deftab
+              |> fold_map (fn {lhs = ty, ...} => ConstNameMangler.declare thy (c, ty)) deftab
               |-> (fn _ => I))) else I
             end) ((#2 o #constants o Consts.dest o #consts o Sign.rep_sg) thy)
       |> (fn (overltab1, overltab2) =>
diff -r f199cb2295fd -r 0d673faf560c src/Pure/Tools/codegen_theorems.ML
--- a/src/Pure/Tools/codegen_theorems.ML	Fri May 05 19:32:34 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Fri May 05 19:32:35 2006 +0200
@@ -439,9 +439,9 @@
       |> filter_typ;
     val thms = case thms_funs
      of [] =>
-          Defs.specifications_of (Theory.defs_of thy) c
-          |> map (PureThy.get_thms thy o Name o fst o snd)
-          |> flat
+          Theory.definitions_of thy c
+          (* FIXME avoid dynamic name space lookup!? (via Thm.get_axiom_i etc.??) *)
+          |> maps (PureThy.get_thms thy o Name o #name)
           |> append (getf_first_list (map (fn f => f thy) (the_funs_extrs thy)) (c, ty))
           |> map (dest_fun thy)
           |> filter_typ