# HG changeset patch
# User wenzelm
# Date 1703876464 -3600
# Node ID 8c9cce335a3dad6d8830074809dfa26c87707620
# Parent  703201dbd4136f77feef544557a3042e6a8844aa
eliminate clone (amending e7796c55d840);

diff -r 703201dbd413 -r 8c9cce335a3d src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Dec 29 19:22:15 2023 +0100
+++ b/src/Pure/logic.ML	Fri Dec 29 20:01:04 2023 +0100
@@ -366,7 +366,7 @@
 fun unconstrainT shyps prop =
   let
     val present = Types.build (prop |> (fold_types o fold_atyps) Types.add_set);
-    val present_sorts = map (fn T => (T, Term.dest_atyp_sort T)) (Types.list_set present);
+    val present_sorts = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present);
 
     val extra = fold (Sorts.remove_sort o #2) present_sorts shyps;
 
diff -r 703201dbd413 -r 8c9cce335a3d src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Dec 29 19:22:15 2023 +0100
+++ b/src/Pure/term.ML	Fri Dec 29 20:01:04 2023 +0100
@@ -122,7 +122,6 @@
 signature TERM =
 sig
   include BASIC_TERM
-  val dest_atyp_sort: typ -> sort
   val aT: sort -> typ
   val itselfT: typ -> typ
   val a_itselfT: typ
@@ -280,10 +279,6 @@
 fun dest_TVar (TVar x) = x
   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
 
-fun dest_atyp_sort (TFree (_, S)) = S
-  | dest_atyp_sort (TVar (_, S)) = S
-  | dest_atyp_sort T = raise TYPE ("dest_atyp_sort", [T], []);
-
 
 (** Discriminators **)