--- 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