# HG changeset patch
# User wenzelm
# Date 1704817543 -3600
# Node ID fe0fffc5d18660317b99fb215d97c7c620800bea
# Parent  664d0cec18fdb6d200042432dcd3df7517e4e9cd
proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);

diff -r 664d0cec18fd -r fe0fffc5d186 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Jan 09 17:10:09 2024 +0100
+++ b/src/Pure/sign.ML	Tue Jan 09 17:25:43 2024 +0100
@@ -307,14 +307,19 @@
 
 fun certify_flags {prop, do_expand} context consts thy tm =
   let
-    val _ = check_vars tm;
-    val tm' = Term.map_types (certify_typ thy) tm;
-    val T = type_check context tm';
-    val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
-    val tm'' = tm'
-      |> Consts.certify {do_expand = do_expand} context (tsig_of thy) consts
-      |> Soft_Type_System.global_purge thy;
-  in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
+    val tsig = tsig_of thy;
+    fun check_term t =
+      let
+        val _ = check_vars t;
+        val t' = Term.map_types (Type.cert_typ_same Type.mode_default tsig) t;
+        val T = type_check context t';
+        val t'' = Consts.certify {do_expand = do_expand} context tsig consts t';
+      in if prop andalso T <> propT then err "Term not of type prop" else (t'', T) end;
+
+    val (tm1, ty1) = check_term tm;
+    val tm' = Soft_Type_System.global_purge thy tm1;
+    val (tm2, ty2) = if tm1 = tm' then (tm1, ty1) else check_term tm';
+  in (if tm = tm2 then tm else tm2, ty2, Term.maxidx_of_term tm2) end;
 
 fun certify_term thy =
   certify_flags {prop = false, do_expand = true} (Context.Theory thy) (consts_of thy) thy;