# HG changeset patch
# User haftmann
# Date 1179567237 -7200
# Node ID 79ee75dc1e593e405a26fde03a348faaa4b9eb96
# Parent  d8c4a02e992a54423d7875c5a3041aaa3a5d1216
constant op @ now named append

diff -r d8c4a02e992a -r 79ee75dc1e59 NEWS
--- a/NEWS	Sat May 19 11:33:34 2007 +0200
+++ b/NEWS	Sat May 19 11:33:57 2007 +0200
@@ -530,6 +530,10 @@
 
 *** HOL ***
 
+* constant "List.op @" now named "List.append".  Use ML antiquotations
+@{const_name List.append} or @{term " ... @ ... "} to circumvent
+possible incompatibilities when working on ML level.
+
 * Constant renames due to introduction of canonical name prefixing for
   class package:
 
diff -r d8c4a02e992a -r 79ee75dc1e59 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat May 19 11:33:57 2007 +0200
@@ -235,7 +235,7 @@
   REVERSE   > List.rev
   LAST      > List.last
   FRONT     > List.butlast
-  APPEND    > "List.op @"
+  APPEND    > List.append
   FLAT      > List.concat
   LENGTH    > Nat.size
   REPLICATE > List.replicate
diff -r d8c4a02e992a -r 79ee75dc1e59 src/HOL/Import/HOL/list.imp
--- a/src/HOL/Import/HOL/list.imp	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Import/HOL/list.imp	Sat May 19 11:33:57 2007 +0200
@@ -33,7 +33,7 @@
   "EXISTS" > "HOL4Compat.list_exists"
   "EVERY" > "List.list_all"
   "CONS" > "List.list.Cons"
-  "APPEND" > "List.op @"
+  "APPEND" > "List.append"
 
 thm_maps
   "list_size_def" > "HOL4Compat.list_size_def"
diff -r d8c4a02e992a -r 79ee75dc1e59 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Induct/SList.thy	Sat May 19 11:33:57 2007 +0200
@@ -159,6 +159,10 @@
   map       :: "('a=>'b) => ('a list => 'b list)" where
   "map f xs = list_rec xs [] (%x l r. f(x)#r)"
 
+no_syntax
+  append :: "'a list => 'a list => 'a list" (infixr "@" 65)
+hide const "List.append"
+
 definition
   append    :: "['a list, 'a list] => 'a list"   (infixr "@" 65) where
   "xs@ys = list_rec xs ys (%x l r. x#r)"
diff -r d8c4a02e992a -r 79ee75dc1e59 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/List.thy	Sat May 19 11:33:57 2007 +0200
@@ -17,7 +17,7 @@
 subsection{*Basic list processing functions*}
 
 consts
-  "@" :: "'a list => 'a list => 'a list"    (infixr 65)
+  append :: "'a list => 'a list => 'a list" (infixr "@" 65)
   filter:: "('a => bool) => 'a list => 'a list"
   concat:: "'a list list => 'a list"
   foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
@@ -309,7 +309,7 @@
 
 fun len (Const("List.list.Nil",_)) acc = acc
   | len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
-  | len (Const("List.op @",_) $ xs $ ys) acc = len xs (len ys acc)
+  | len (Const("List.append",_) $ xs $ ys) acc = len xs (len ys acc)
   | len (Const("List.rev",_) $ xs) acc = len xs acc
   | len (Const("List.map",_) $ _ $ xs) acc = len xs acc
   | len t (ts,n) = (t::ts,n);
@@ -447,7 +447,7 @@
 
 fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
   (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
-  | last (Const("List.op @",_) $ _ $ ys) = last ys
+  | last (Const("List.append",_) $ _ $ ys) = last ys
   | last t = t;
 
 fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
@@ -455,7 +455,7 @@
 
 fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
   (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
-  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
+  | butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys
   | butlast xs = Const("List.list.Nil",fastype_of xs);
 
 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
@@ -469,7 +469,7 @@
         val lhs1 = butlast lhs and rhs1 = butlast rhs;
         val Type(_,listT::_) = eqT
         val appT = [listT,listT] ---> listT
-        val app = Const("List.op @",appT)
+        val app = Const("List.append",appT)
         val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
         val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
diff -r d8c4a02e992a -r 79ee75dc1e59 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat May 19 11:33:57 2007 +0200
@@ -204,7 +204,7 @@
           val pi2 = Free ("pi2", mk_permT T);
           val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
           val cnil  = Const ("List.list.Nil", mk_permT T);
-          val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
+          val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
           val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
           (* nil axiom *)
           val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
diff -r d8c4a02e992a -r 79ee75dc1e59 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Sat May 19 11:33:57 2007 +0200
@@ -206,7 +206,7 @@
 val fresh_def = thm "fresh_def";
 val supp_def = thm "supp_def";
 val rev_simps = thms "rev.simps";
-val app_simps = thms "op @.simps";
+val app_simps = thms "append.simps";
 
 val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
 
@@ -402,7 +402,7 @@
                 (map (fn ((s, T), x) =>
                     let val perm = Const (s, permT --> T --> T)
                     in HOLogic.mk_eq
-                      (perm $ (Const ("List.op @", permT --> permT --> permT) $
+                      (perm $ (Const ("List.append", permT --> permT --> permT) $
                          pi1 $ pi2) $ Free (x, T),
                        perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
                     end)
diff -r d8c4a02e992a -r 79ee75dc1e59 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Tools/refute.ML	Sat May 19 11:33:57 2007 +0200
@@ -704,7 +704,7 @@
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
       | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
-      | Const ("List.op @", _)          => t
+      | Const ("List.append", _)          => t
       | Const ("Lfp.lfp", _)            => t
       | Const ("Gfp.gfp", _)            => t
       | Const ("fst", _)                => t
@@ -895,7 +895,7 @@
       | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
           collect_type_axioms (axs, T)
-      | Const ("List.op @", T)          => collect_type_axioms (axs, T)
+      | Const ("List.append", T)          => collect_type_axioms (axs, T)
       | Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)
       | Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)
       | Const ("fst", T)                => collect_type_axioms (axs, T)
@@ -2727,13 +2727,13 @@
   (* theory -> model -> arguments -> Term.term ->
     (interpretation * model * arguments) option *)
 
-  (* only an optimization: 'op @' could in principle be interpreted with *)
+  (* only an optimization: 'append' could in principle be interpreted with *)
   (* interpreters available already (using its definition), but the code *)
   (* below is more efficient                                             *)
 
   fun List_append_interpreter thy model args t =
     case t of
-      Const ("List.op @", Type ("fun", [Type ("List.list", [T]), Type ("fun",
+      Const ("List.append", Type ("fun", [Type ("List.list", [T]), Type ("fun",
         [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
       let
         val (i_elem, _, _) = interpret thy model
@@ -3215,7 +3215,7 @@
      add_interpreter "Nat_HOL.plus"       Nat_plus_interpreter #>
      add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
      add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
-     add_interpreter "List.op @" List_append_interpreter #>
+     add_interpreter "List.append" List_append_interpreter #>
      add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
      add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
      add_interpreter "fst" Product_Type_fst_interpreter #>
diff -r d8c4a02e992a -r 79ee75dc1e59 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML	Sat May 19 11:33:57 2007 +0200
@@ -117,7 +117,7 @@
 		   ("op :", "in"),
 		   ("op Un", "union"),
 		   ("op Int", "inter"),
-		   ("List.op @", "append"),
+		   ("List.append", "append"),
 		   ("ATP_Linkup.fequal", "fequal"),
 		   ("ATP_Linkup.COMBI", "COMBI"),
 		   ("ATP_Linkup.COMBK", "COMBK"),