# HG changeset patch
# User wenzelm
# Date 1246912860 -7200
# Node ID 99ac0321cd47b4a29ff56b5032cd6e6d28b9b208
# Parent  d5f186aa0beda31177f79b4fb064158567da98d3
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;

diff -r d5f186aa0bed -r 99ac0321cd47 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jul 06 21:24:30 2009 +0200
+++ b/src/Pure/sign.ML	Mon Jul 06 22:41:00 2009 +0200
@@ -27,7 +27,7 @@
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
-  val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
+  val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
   val is_logtype: theory -> string -> bool
   val typ_instance: theory -> typ * typ -> bool
   val typ_equiv: theory -> typ * typ -> bool
diff -r d5f186aa0bed -r 99ac0321cd47 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Jul 06 21:24:30 2009 +0200
+++ b/src/Pure/sorts.ML	Mon Jul 06 22:41:00 2009 +0200
@@ -62,7 +62,7 @@
      type_constructor: string -> ('a * class) list list -> class -> 'a,
      type_variable: typ -> ('a * class) list} ->
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
-  val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
+  val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
 end;
 
 structure Sorts: SORTS =
@@ -432,18 +432,17 @@
 fun witness_sorts algebra types hyps sorts =
   let
     fun le S1 S2 = sort_le algebra (S1, S2);
-    fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
-    fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE;
+    fun get S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
     fun mg_dom t S = SOME (mg_domain algebra t S) handle CLASS_ERROR _ => NONE;
 
     fun witn_sort _ [] solved_failed = (SOME (propT, []), solved_failed)
       | witn_sort path S (solved, failed) =
           if exists (le S) failed then (NONE, (solved, failed))
           else
-            (case get_first (get_solved S) solved of
+            (case get_first (get S) solved of
               SOME w => (SOME w, (solved, failed))
             | NONE =>
-                (case get_first (get_hyp S) hyps of
+                (case get_first (get S) hyps of
                   SOME w => (SOME w, (w :: solved, failed))
                 | NONE => witn_types path types S (solved, failed)))
 
diff -r d5f186aa0bed -r 99ac0321cd47 src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Jul 06 21:24:30 2009 +0200
+++ b/src/Pure/type.ML	Mon Jul 06 22:41:00 2009 +0200
@@ -27,7 +27,7 @@
   val inter_sort: tsig -> sort * sort -> sort
   val cert_class: tsig -> class -> class
   val cert_sort: tsig -> sort -> sort
-  val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
+  val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list
   type mode
   val mode_default: mode
   val mode_syntax: mode