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/syntax_phases.ML
changeset 42290 b1f544c84040
parent 42289 dafae095d733
child 42294 0f4372a2d2e4 
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 16:34:14 2011 +0200
@@ -434,9 +434,9 @@
     fun term_of (Type (a, Ts)) =
           Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
       | term_of (TFree (x, S)) =
-          if is_some (Term_Position.decode x) then Lexicon.free x
-          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
-      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
+          if is_some (Term_Position.decode x) then Syntax.free x
+          else of_sort (Lexicon.const "_tfree" $ Syntax.free x) S
+      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Syntax.var xi) S;
   in term_of ty end;
 
 
@@ -514,11 +514,11 @@
     fun prune_typs (t_seen as (Const _, _)) = t_seen
       | prune_typs (t as Free (x, ty), seen) =
           if ty = dummyT then (t, seen)
-          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
+          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
           else (t, t :: seen)
       | prune_typs (t as Var (xi, ty), seen) =
           if ty = dummyT then (t, seen)
-          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
+          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
           else (t, t :: seen)
       | prune_typs (t_seen as (Bound _, _)) = t_seen
       | prune_typs (Abs (x, ty, t), seen) =
@@ -534,11 +534,11 @@
       (case strip_comb tm of
         (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
       | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
-          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
-          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
+          Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
       | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
-          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
       | (const as Const (c, T), ts) =>
isabelle