# HG changeset patch
# User wenzelm
# Date 960914099 -7200
# Node ID b0dd884b1848faf1c728fedd67354cf1151531c3
# Parent  2b537d9e6f495b29293b807e8b69adb0cd0bf179
rename @case to _case_syntax (improves on low-level errors);

diff -r 2b537d9e6f49 -r b0dd884b1848 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 13 18:33:55 2000 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 13 18:34:59 2000 +0200
@@ -93,10 +93,10 @@
 
   (* Case expressions *)
 
-  "@case"       :: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
-  "@case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
+  "_case_syntax":: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
+  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
   ""            :: "case_syn => cases_syn"               ("_")
-  "@case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
+  "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
 
 translations
   "x ~= y"                == "~ (x = y)"
@@ -119,8 +119,8 @@
   "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
-  "@case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
-(*"@case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
+  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
+(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
 
 syntax (symbols output)
   "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)
diff -r 2b537d9e6f49 -r b0dd884b1848 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jun 13 18:33:55 2000 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jun 13 18:34:59 2000 +0200
@@ -60,10 +60,10 @@
   "Mu "		:: [idts, 'a pred] => 'a pred		("(3mu _./ _)" 1000)
   "Nu "		:: [idts, 'a pred] => 'a pred		("(3nu _./ _)" 1000)
   
-  "@case"       :: ['a, cases_syn] => 'b            ("(case*_* / _ / esac*)" 10)
-  "@case1"      :: ['a, 'b] => case_syn             ("(2*= _ :/ _;)" 10)
+  "_case_syntax":: ['a, cases_syn] => 'b            ("(case*_* / _ / esac*)" 10)
+  "_case1"      :: ['a, 'b] => case_syn             ("(2*= _ :/ _;)" 10)
   ""            :: case_syn => cases_syn            ("_")
-  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ _")
+  "_case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ _")
 (* Terms containing a case statement must be post-processed with the function  *)
 (* transform_case, defined in MuCalculus.ML. There, all asterikses before the  *)
 (* "=" will be replaced by the expression between the two asterikses following *)
diff -r 2b537d9e6f49 -r b0dd884b1848 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Tue Jun 13 18:33:55 2000 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Jun 13 18:34:59 2000 +0200
@@ -366,7 +366,7 @@
         val k = length cargs;
         val xs = map (fn i => Variable ("x" ^ string_of_int i)) (i upto i + k - 1);
         val t = Variable ("t" ^ string_of_int j);
-        val ast = Syntax.mk_appl (Constant "@case1")
+        val ast = Syntax.mk_appl (Constant "_case1")
           [Syntax.mk_appl (Constant (Sign.base_name cname)) xs, t];
         val ast' = foldr (fn (x, y) =>
           Syntax.mk_appl (Constant "_abs") [x, y]) (xs, t)
@@ -374,7 +374,7 @@
         (case constrs of
             [] => (ast, [ast'])
           | cs => let val (ast'', asts) = mk_asts (i + k) (j + 1) cs
-              in (Syntax.mk_appl (Constant "@case2") [ast, ast''],
+              in (Syntax.mk_appl (Constant "_case2") [ast, ast''],
                   ast'::asts)
               end)
       end;
@@ -382,7 +382,7 @@
     fun mk_trrule ((_, (_, _, constrs)), tname) =
       let val (ast, asts) = mk_asts 1 1 constrs
       in Syntax.ParsePrintRule
-        (Syntax.mk_appl (Constant "@case") [Variable "t", ast],
+        (Syntax.mk_appl (Constant "_case_syntax") [Variable "t", ast],
          Syntax.mk_appl (Constant (tname ^ "_case"))
            (asts @ [Variable "t"]))
       end
diff -r 2b537d9e6f49 -r b0dd884b1848 src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Tue Jun 13 18:33:55 2000 +0200
+++ b/src/HOLCF/domain/syntax.ML	Tue Jun 13 18:34:59 2000 +0200
@@ -70,7 +70,7 @@
 	fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
 					 (string_of_int m));
 	fun app s (l,r)   = mk_appl (Constant s) [l,r];
-	fun case1 n (con,mx,args) = mk_appl (Constant "@case1")
+	fun case1 n (con,mx,args) = mk_appl (Constant "_case1")
 		 [foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
 		  expvar n];
 	fun arg1 n (con,_,args) = if args = [] then expvar n 
@@ -78,8 +78,8 @@
 		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
   in
     ParsePrintRule
-      (mk_appl (Constant "@case") [Variable "x", foldr'
-				(fn (c,cs) => mk_appl (Constant"@case2") [c,cs])
+      (mk_appl (Constant "_case_syntax") [Variable "x", foldr'
+				(fn (c,cs) => mk_appl (Constant"_case2") [c,cs])
 				 (mapn case1 1 cons')],
        mk_appl (Constant "Rep_CFun") [foldl 
 				(fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ])