Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Context.the_context;
authorwenzelm
Wed, 10 Jun 1998 18:07:07 +0200
changeset 5028 61c10aad3d71
parent 5027 4b1fd9813003
child 5029 bb542ac4c94d
Context.the_context;
src/Provers/classical.ML file | annotate | diff | comparison | revisions
src/Provers/simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/classical.ML	Wed Jun 10 17:56:57 1998 +0200
+++ b/src/Provers/classical.ML	Wed Jun 10 18:07:07 1998 +0200
@@ -767,8 +767,8 @@
 fun CLASET tacf state = tacf (claset_of_sg (sign_of_thm state)) state;
 fun CLASET' tacf i state = tacf (claset_of_sg (sign_of_thm state)) i state;
 
-val claset = claset_of o Context.get_context;
-val claset_ref = claset_ref_of_sg o sign_of o Context.get_context;
+val claset = claset_of o Context.the_context;
+val claset_ref = claset_ref_of_sg o sign_of o Context.the_context;
 
 
 (* change claset *)
--- a/src/Provers/simplifier.ML	Wed Jun 10 17:56:57 1998 +0200
+++ b/src/Provers/simplifier.ML	Wed Jun 10 18:07:07 1998 +0200
@@ -284,8 +284,8 @@
 fun SIMPSET tacf state = tacf (simpset_of_sg (sign_of_thm state)) state;
 fun SIMPSET' tacf i state = tacf (simpset_of_sg (sign_of_thm state)) i state;
 
-val simpset = simpset_of o Context.get_context;
-val simpset_ref = simpset_ref_of_sg o sign_of o Context.get_context;
+val simpset = simpset_of o Context.the_context;
+val simpset_ref = simpset_ref_of_sg o sign_of o Context.the_context;
 
 
 (* change global simpset *)
isabelle