# HG changeset patch
# User wenzelm
# Date 908894181 -7200
# Node ID 898429dbb162b8bc92da87d409e17390d7ac8f19
# Parent  39af7b3dd1c4506d56408cbaa726981877c3edb3
fixed Syntax module;

diff -r 39af7b3dd1c4 -r 898429dbb162 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Tue Oct 20 16:35:37 1998 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Oct 20 16:36:21 1998 +0200
@@ -370,15 +370,15 @@
         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 = Ast.mk_appl (Constant "@case1")
-          [Ast.mk_appl (Constant (Sign.base_name cname)) xs, t];
+        val ast = Syntax.mk_appl (Constant "@case1")
+          [Syntax.mk_appl (Constant (Sign.base_name cname)) xs, t];
         val ast' = foldr (fn (x, y) =>
-          Ast.mk_appl (Constant "_abs") [x, y]) (xs, t)
+          Syntax.mk_appl (Constant "_abs") [x, y]) (xs, t)
       in
         (case constrs of
             [] => (ast, [ast'])
           | cs => let val (ast'', asts) = mk_asts (i + k) (j + 1) cs
-              in (Ast.mk_appl (Constant "@case2") [ast, ast''],
+              in (Syntax.mk_appl (Constant "@case2") [ast, ast''],
                   ast'::asts)
               end)
       end;
@@ -386,8 +386,8 @@
     fun mk_trrule ((_, (_, _, constrs)), tname) =
       let val (ast, asts) = mk_asts 1 1 constrs
       in Syntax.ParsePrintRule
-        (Ast.mk_appl (Constant "@case") [Variable "t", ast],
-         Ast.mk_appl (Constant (tname ^ "_case"))
+        (Syntax.mk_appl (Constant "@case") [Variable "t", ast],
+         Syntax.mk_appl (Constant (tname ^ "_case"))
            (asts @ [Variable "t"]))
       end