Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/proofterm.ML
changeset 16536 c5744af6b28a
parent 16458 4c6fd0c01d28
child 16787 b6b6e2faaa41 
--- a/src/Pure/proofterm.ML	Wed Jun 22 19:41:20 2005 +0200
+++ b/src/Pure/proofterm.ML	Wed Jun 22 19:41:22 2005 +0200
@@ -107,7 +107,7 @@
     (string * (typ list -> proof -> proof option)) list -> proof -> proof
   val rewrite_proof_notypes : (proof * proof) list *
     (string * (typ list -> proof -> proof option)) list -> proof -> proof
-  val init : theory -> theory
+  val init_data: theory -> theory
   
 end
 
@@ -1107,7 +1107,7 @@
   fun print _ _ = ();
 end);
 
-val init = ProofData.init;
+val init_data = ProofData.init;
 
 fun add_prf_rrules rs thy =
   let val r = ProofData.get thy
isabelle