# HG changeset patch
# User wenzelm
# Date 1191859987 -7200
# Node ID c74ad8782eeb5355a48cbb1ca3f702317d9955af
# Parent  bfb2e82b61fece6e635be49d4822168df5ef1527
Codegen.is_instance: raw match, ignore sort constraints;
replaced get_axiom by authentic get_axiom_i;

diff -r bfb2e82b61fe -r c74ad8782eeb src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Oct 08 18:13:06 2007 +0200
+++ b/src/Pure/codegen.ML	Mon Oct 08 18:13:07 2007 +0200
@@ -64,7 +64,7 @@
   val if_library: 'a -> 'a -> 'a
   val get_defn: theory -> deftab -> string -> typ ->
     ((typ * (string * (term list * term))) * int option) option
-  val is_instance: theory -> typ -> typ -> bool
+  val is_instance: typ -> typ -> bool
   val parens: Pretty.T -> Pretty.T
   val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
   val eta_expand: term -> term list -> int -> term
@@ -530,11 +530,11 @@
 
 (**** retrieve definition of constant ****)
 
-fun is_instance thy T1 T2 =
-  Sign.typ_instance thy (T1, Logic.legacy_varifyT T2);
+fun is_instance T1 T2 =
+  Type.raw_instance (T1, Logic.legacy_varifyT T2);
 
 fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
-  s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
+  s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
 
 fun get_aux_code xs = map_filter (fn (m, code) =>
   if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs;
@@ -554,7 +554,7 @@
       end handle TERM _ => NONE;
     fun add_def thyname (name, t) = (case dest t of
         NONE => I
-      | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of
+      | SOME _ => (case dest (prep_def (Thm.get_axiom_i thy name)) of
           NONE => I
         | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, [])
             (cons (T, (thyname, split_last (rename_terms (args @ [rhs])))))))
@@ -565,7 +565,7 @@
 fun get_defn thy defs s T = (case Symtab.lookup defs s of
     NONE => NONE
   | SOME ds =>
-      let val i = find_index (is_instance thy T o fst) ds
+      let val i = find_index (is_instance T o fst) ds
       in if i >= 0 then
           SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i)
         else NONE