# HG changeset patch
# User huffman
# Date 1291215054 28800
# Node ID f2c9ebbe04aaeb514348bab1fb50654f6b0beb94
# Parent  225698654b2aafd39e2a3f747d1cd736c3b53c41# Parent  df8c7dc30214daded172e409934a8e89b0639bd5
merged

diff -r df8c7dc30214 -r f2c9ebbe04aa src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Dec 01 06:50:54 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 =