domain package generates non-authentic syntax rules for parsing only
authorhuffman
Wed, 01 Dec 2010 06:48:40 -0800
changeset 40853 225698654b2a
parent 40846 5a2ae8cc9d0e
child 40854 f2c9ebbe04aa
domain package generates non-authentic syntax rules for parsing only
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 =