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/type_ext.ML
changeset 20854 f9cf9e62d11c
parent 19305 5c16895d548b
child 22704 f67607c3e56e 
--- a/src/Pure/Syntax/type_ext.ML	Wed Oct 04 14:14:33 2006 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Oct 04 14:17:38 2006 +0200
@@ -55,13 +55,13 @@
 fun raw_term_sorts tm =
   let
     fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env =
-          ((x, ~1), sort_of_term cs) ins env
+          insert (op =) ((x, ~1), sort_of_term cs) env
       | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env =
-          ((x, ~1), sort_of_term cs) ins env
+          insert (op =) ((x, ~1), sort_of_term cs) env
       | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env =
-          (xi, sort_of_term cs) ins env
+          insert (op =) (xi, sort_of_term cs) env
       | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env =
-          (xi, sort_of_term cs) ins env
+          insert (op =) (xi, sort_of_term cs) env
       | add_env (Abs (_, _, t)) env = add_env t env
       | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
       | add_env _ env = env;
isabelle