src/Provers/quantifier1.ML

     val n = length xs;
     val Q = if n = 0 then P else renumber 0 n P;
   in quant xs (qC $ Abs (x, T, Q)) end;
 
 fun rearrange_all ctxt ct =
-  (case term_of ct of
+  (case Thm.term_of ct of
     F as (all as Const (q, _)) $ Abs (x, T, P) =>
       (case extract_quant extract_imp q P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify all x T xs (Data.imp $ eq $ Q)
           in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end)
   | _ => NONE);
 
 fun rearrange_ball tac ctxt ct =
-  (case term_of ct of
+  (case Thm.term_of ct of
     F as Ball $ A $ Abs (x, T, P) =>
       (case extract_imp true [] P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           if not (null xs) then NONE

             let val R = Data.imp $ eq $ Q
             in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
   | _ => NONE);
 
 fun rearrange_ex ctxt ct =
-  (case term_of ct of
+  (case Thm.term_of ct of
     F as (ex as Const (q, _)) $ Abs (x, T, P) =>
       (case extract_quant extract_conj q P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify ex x T xs (Data.conj $ eq $ Q)
           in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end)
   | _ => NONE);
 
 fun rearrange_bex tac ctxt ct =
-  (case term_of ct of
+  (case Thm.term_of ct of
     F as Bex $ A $ Abs (x, T, P) =>
       (case extract_conj true [] P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           if not (null xs) then NONE
           else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
   | _ => NONE);
 
 fun rearrange_Collect tac ctxt ct =
-  (case term_of ct of
+  (case Thm.term_of ct of
     F as Collect $ Abs (x, T, P) =>
       (case extract_conj true [] P of
         NONE => NONE
       | SOME (_, eq, Q) =>
           let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)