# HG changeset patch
# User huffman
# Date 1291214920 28800
# Node ID 225698654b2aafd39e2a3f747d1cd736c3b53c41
# Parent  5a2ae8cc9d0e619c68a300a4e496cdfe19740758
domain package generates non-authentic syntax rules for parsing only

diff -r 5a2ae8cc9d0e -r 225698654b2a src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Dec 01 11:45:37 2010 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Dec 01 06:48:40 2010 -0800
@@ -464,13 +464,13 @@
           if n = m then arg1 (n, c) else (Constant @{const_syntax UU})
       val case_constant = Constant (syntax (case_const dummyT))
       fun case_trans authentic =
-          ParsePrintRule
+          (if authentic then ParsePrintRule else ParseRule)
             (app "_case_syntax"
               (Variable "x",
                foldr1 (app "_case2") (map_index (case1 authentic) spec)),
              capp (capps (case_constant, map_index arg1 spec), Variable "x"))
       fun one_abscon_trans authentic (n, c) =
-          ParsePrintRule
+          (if authentic then ParsePrintRule else ParseRule)
             (cabs (con1 authentic n c, expvar n),
              capps (case_constant, map_index (when1 n) spec))
       fun abscon_trans authentic =