src/Pure/Proof/proof_rewrite_rules.ML

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -10,12 +10,12 @@
   val rprocs : bool ->
     (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
   val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
-  val elim_defs : Proof.context -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
+  val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
   val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
   val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
   val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
-  val mk_of_sort_proof : Proof.context -> term option list -> typ * sort -> Proofterm.proof list
-  val expand_of_class : Proof.context -> typ list -> term option list -> Proofterm.proof ->
+  val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+  val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
     (Proofterm.proof * Proofterm.proof) option
 end;
 
@@ -250,7 +250,7 @@
       | (_, []) => (prf, false)
       | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
 
-fun elim_defs ctxt r defs prf =
+fun elim_defs thy r defs prf =
   let
     val defs' = map (Logic.dest_equals o
       map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
@@ -265,9 +265,9 @@
               then I
               else cons (name, SOME prop)
             | _ => I) [prf] [];
-      in Proofterm.expand_proof ctxt thms end;
+      in Proofterm.expand_proof thy thms end;
   in
-    rewrite_terms (Pattern.rewrite_term (Proof_Context.theory_of ctxt) defs' [])
+    rewrite_terms (Pattern.rewrite_term thy defs' [])
       (fst (insert_refl defnames [] (f prf)))
   end;
 
@@ -340,7 +340,7 @@
 
 (**** expand OfClass proofs ****)
 
-fun mk_of_sort_proof ctxt hs (T, S) =
+fun mk_of_sort_proof thy hs (T, S) =
   let
     val hs' = map
       (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
@@ -354,19 +354,18 @@
         ~1 => error "expand_of_class: missing class hypothesis"
       | i => PBound i;
     fun reconstruct prf prop = prf |>
-      Proofterm.reconstruct_proof ctxt prop |>
-      Proofterm.expand_proof ctxt [("", NONE)] |>
+      Proofterm.reconstruct_proof thy prop |>
+      Proofterm.expand_proof thy [("", NONE)] |>
       Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
   in
     map2 reconstruct
-      (Proofterm.of_sort_proof (Proof_Context.theory_of ctxt)
-        (OfClass o apfst Type.strip_sorts) (subst T, S))
+      (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
       (Logic.mk_of_sort (T, S))
   end;
 
-fun expand_of_class ctxt Ts hs (OfClass (T, c)) =
-      mk_of_sort_proof ctxt hs (T, [c]) |>
+fun expand_of_class thy Ts hs (OfClass (T, c)) =
+      mk_of_sort_proof thy hs (T, [c]) |>
       hd |> rpair Proofterm.no_skel |> SOME
-  | expand_of_class ctxt Ts hs _ = NONE;
+  | expand_of_class thy Ts hs _ = NONE;
 
 end;