# HG changeset patch
# User wenzelm
# Date 1729623234 -7200
# Node ID b35c2aa05fcffd78dc7e27c6a57f1972bb3d296f
# Parent  ae0ccabd0aabcca8f39c77a6a87a329b23799d28
proper treatment of position constraints;

diff -r ae0ccabd0aab -r b35c2aa05fcf src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Tue Oct 22 20:05:23 2024 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Tue Oct 22 20:53:54 2024 +0200
@@ -121,18 +121,27 @@
             then Syntax.parse_prop ctxt3 term
             else Syntax.parse_term ctxt3 term;
 
-          fun drop_judgment_dummy t =
+          val judgment_name = Object_Logic.judgment_name ctxt;
+
+          fun dest_judgment_dummy t =
             (case t of
-              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);
+              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));
 
           val pats =
             map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts