# HG changeset patch
# User wenzelm
# Date 1729766688 -7200
# Node ID b43192613888f45c611c49d02d15840998294a75
# Parent  89ea66c2045b6e75c75132295d8d19ad6dd618aa
revert b35c2aa05fcf: redundant due to 89ea66c2045b, if object-logic judgment lacks delimiters;

diff -r 89ea66c2045b -r b43192613888 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Thu Oct 24 12:42:41 2024 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Thu Oct 24 12:44:48 2024 +0200
@@ -121,27 +121,18 @@
             then Syntax.parse_prop ctxt3 term
             else Syntax.parse_term ctxt3 term;
 
-          val judgment_name = Object_Logic.judgment_name ctxt;
-
-          fun dest_judgment_dummy t =
+          fun drop_judgment_dummy t =
             (case t of
-              Const (c, _) $
-              (Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $ \<^Const_>\<open>Pure.dummy_pattern _\<close>) =>
-                if c = judgment_name then SOME T else NONE
-            | Const (\<^syntax_const>\<open>_type_constraint_\<close>, _) $ Const (c, _) $
-              (Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $ \<^Const_>\<open>Pure.dummy_pattern _\<close>) =>
-                if c = judgment_name then SOME T else NONE
-            | _ => NONE);
-
-          fun drop_judgment_dummy t =
-            (case dest_judgment_dummy t of
-              SOME T =>
-                Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $ \<^Const>\<open>Pure.dummy_pattern \<^Type>\<open>prop\<close>\<close>
-            | NONE =>
-                (case t of
-                  t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2
-                | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b)
-                | _ => t));
+              Const (judgment, _) $
+                (Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $
+                  Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, _)) =>
+                if judgment = Object_Logic.judgment_name ctxt then
+                    Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $
+                      Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, propT)
+                else t
+            | t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2
+            | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b)
+            | _ => t);
 
           val pats =
             map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts