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/Syntax/syn_trans.ML
changeset 26424 a6cad32a27b0
parent 23963 c2ee97a963db
child 28628 06737d425249 
--- a/src/Pure/Syntax/syn_trans.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -149,7 +149,7 @@
 
 (* meta conjunction *)
 
-fun conjunction_tr [t, u] = Lexicon.const "ProtoPure.conjunction" $ t $ u
+fun conjunction_tr [t, u] = Lexicon.const "Pure.conjunction" $ t $ u
   | conjunction_tr ts = raise TERM ("conjunction_tr", ts);
 
 
@@ -159,7 +159,7 @@
       Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty)
   | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
 
-fun term_tr [t] = Lexicon.const "ProtoPure.term" $ t
+fun term_tr [t] = Lexicon.const "Pure.term" $ t
   | term_tr ts = raise TERM ("term_tr", ts);
 
 
@@ -341,7 +341,7 @@
     fun is_prop Ts t =
       fastype_of1 (Ts, t) = propT handle TERM _ => false;
 
-    fun is_term (Const ("ProtoPure.term", _) $ _) = true
+    fun is_term (Const ("Pure.term", _) $ _) = true
       | is_term _ = false;
 
     fun tr' _ (t as Const _) = t
isabelle