# HG changeset patch
# User haftmann
# Date 1587365889 -7200
# Node ID 7c2f4dd48fb6f57291412b6469819224e7263fe9
# Parent  af1381b565d692d0814ecf3d914ea0bb1638b5fe
more robust judgment handling

diff -r af1381b565d6 -r 7c2f4dd48fb6 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Sun Apr 19 22:58:32 2020 +0100
+++ b/src/Provers/quantifier1.ML	Mon Apr 20 08:58:09 2020 +0200
@@ -117,9 +117,13 @@
 fun extract_conj_from_judgment ctxt fst xs t =
   if Object_Logic.is_judgment ctxt t
   then
-    (case extract_conj fst xs (Object_Logic.drop_judgment ctxt t) of
-      NONE => NONE
-    | SOME (xs, eq, P) => SOME (xs, Object_Logic.ensure_propT ctxt eq, Object_Logic.ensure_propT ctxt P))
+    let
+      val judg $ t' = t
+    in
+      case extract_conj fst xs t' of
+          NONE => NONE
+        | SOME (xs, eq, P) => SOME (xs, judg $ eq, judg $ P)
+    end
   else NONE;
 
 fun extract_implies ctxt fst xs t =