src/Pure/proofterm.ML

 
 fun OfClasst (T, c) =
   let val U = Term.itselfT T --> propT
   in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
 
+fun term_of _ (PThm ({name, types = Ts, ...}, _)) =
+      fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT))
+  | term_of _ (PAxm (name, _, Ts)) =
+      fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
+  | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
+  | term_of _ (PBound i) = Bound i
+  | term_of Ts (Abst (s, opT, prf)) =
+      let val T = the_default dummyT opT in
+        Const ("Pure.Abst", (T --> proofT) --> proofT) $
+          Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
+      end
+  | term_of Ts (AbsP (s, t, prf)) =
+      AbsPt $ the_default Term.dummy_prop t $
+        Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
+  | term_of Ts (prf1 %% prf2) =
+      AppPt $ term_of Ts prf1 $ term_of Ts prf2
+  | term_of Ts (prf % opt) =
+      let
+        val t = the_default Term.dummy opt;
+        val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
+      in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
+  | term_of _ (Hyp t) = Hypt $ t
+  | term_of _ (Oracle (_, t, _)) = Oraclet $ t
+  | term_of _ MinProof = MinProoft;
+
 in
 
-fun thm_const_default (_: proof_serial) name = Long_Name.append "thm" name;
-fun axm_const_default name = Long_Name.append "axm" name;
-
-fun term_of
-   {thm_const: proof_serial -> string -> string,
-    axm_const: string -> string} =
-  let
-    fun term _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
-          fold AppT (these Ts) (Const (thm_const i name, proofT))
-      | term _ (PAxm (name, _, Ts)) =
-          fold AppT (these Ts) (Const (axm_const name, proofT))
-      | term _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
-      | term _ (PBound i) = Bound i
-      | term Ts (Abst (s, opT, prf)) =
-          let val T = the_default dummyT opT in
-            Const ("Pure.Abst", (T --> proofT) --> proofT) $
-              Abs (s, T, term (T::Ts) (incr_pboundvars 1 0 prf))
-          end
-      | term Ts (AbsP (s, t, prf)) =
-          AbsPt $ the_default Term.dummy_prop t $
-            Abs (s, proofT, term (proofT::Ts) (incr_pboundvars 0 1 prf))
-      | term Ts (prf1 %% prf2) =
-          AppPt $ term Ts prf1 $ term Ts prf2
-      | term Ts (prf % opt) =
-          let
-            val t = the_default Term.dummy opt;
-            val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
-          in Const ("Pure.Appt", proofT --> T --> proofT) $ term Ts prf $ t end
-      | term _ (Hyp t) = Hypt $ t
-      | term _ (Oracle (_, t, _)) = Oraclet $ t
-      | term _ MinProof = MinProoft;
-  in term [] end;
-
-val term_of_proof = term_of {thm_const = thm_const_default, axm_const = axm_const_default};
+val term_of_proof = term_of [];
 
 end;