# HG changeset patch
# User haftmann
# Date 1266573980 -3600
# Node ID 1c9866c5f6fbd39c6df823d5b16b959e6d78597b
# Parent  9f35be9c296016559b190f7c31bdf391196aa4f0
simplified

diff -r 9f35be9c2960 -r 1c9866c5f6fb src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Feb 19 11:06:20 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Feb 19 11:06:20 2010 +0100
@@ -314,9 +314,7 @@
   else false
 *)
 
-(* must be exported in code.ML *)
-(* TODO: is there copy in the core? *)
-fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
+val is_constr = Code.is_constr;
 
 fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
   let
diff -r 9f35be9c2960 -r 1c9866c5f6fb src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Feb 19 11:06:20 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Feb 19 11:06:20 2010 +0100
@@ -216,14 +216,6 @@
   map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
     o maps (#params o AxClass.get_info thy);
 
-fun typargs_rhss thy c cert =
-  let
-    val ((vs, _), equations) = Code.equations_cert thy cert;
-    val rhss = [] |> (fold o fold o fold_aterms)
-      (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, ty)) | _ => I)
-        (map (op :: o swap) equations);
-  in (vs, rhss) end;
-
 
 (* data structures *)
 
@@ -262,7 +254,7 @@
    of SOME (lhs, cert) => ((lhs, []), cert)
     | NONE => let
         val cert = Code.get_cert thy (preprocess thy) c;
-        val (lhs, rhss) = typargs_rhss thy c cert;
+        val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
       in ((lhs, rhss), cert) end;
 
 fun obtain_instance thy arities (inst as (class, tyco)) =
@@ -395,7 +387,7 @@
     val lhs = map_index (fn (k, (v, _)) =>
       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
     val cert = Code.constrain_cert thy (map snd lhs) proto_cert;
-    val (vs, rhss') = typargs_rhss thy c cert;
+    val (vs, rhss') = Code.typargs_deps_of_cert thy cert;
     val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
   in (map (pair c) rhss' @ rhss, eqngr') end;