more robust judgment handling

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