--- 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