1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Apr 05 13:07:40 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Apr 05 14:25:18 2011 +0200
     1.3 @@ -442,16 +442,14 @@
     1.4      (* define syntax for case combinator *)
     1.5      (* TODO: re-implement case syntax using a parse translation *)
     1.6      local
     1.7 -      open Syntax
     1.8        fun syntax c = Syntax.mark_const (fst (dest_Const c))
     1.9        fun xconst c = Long_Name.base_name (fst (dest_Const c))
    1.10 -      fun c_ast authentic con =
    1.11 -          Constant (if authentic then syntax con else xconst con)
    1.12 +      fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
    1.13        fun showint n = string_of_int (n+1)
    1.14 -      fun expvar n = Variable ("e" ^ showint n)
    1.15 -      fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m)
    1.16 +      fun expvar n = Ast.Variable ("e" ^ showint n)
    1.17 +      fun argvar n (m, _) = Ast.Variable ("a" ^ showint n ^ "_" ^ showint m)
    1.18        fun argvars n args = map_index (argvar n) args
    1.19 -      fun app s (l, r) = mk_appl (Constant s) [l, r]
    1.20 +      fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r]
    1.21        val cabs = app "_cabs"
    1.22        val capp = app @{const_syntax Rep_cfun}
    1.23        val capps = Library.foldl capp
    1.24 @@ -460,22 +458,21 @@
    1.25        fun case1 authentic (n, c) =
    1.26            app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
    1.27        fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
    1.28 -      fun when1 n (m, c) =
    1.29 -          if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
    1.30 -      val case_constant = Constant (syntax (case_const dummyT))
    1.31 +      fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
    1.32 +      val case_constant = Ast.Constant (syntax (case_const dummyT))
    1.33        fun case_trans authentic =
    1.34 -          (if authentic then Parse_Print_Rule else Parse_Rule)
    1.35 -            (app "_case_syntax"
    1.36 -              (Variable "x",
    1.37 -               foldr1 (app "_case2") (map_index (case1 authentic) spec)),
    1.38 -             capp (capps (case_constant, map_index arg1 spec), Variable "x"))
    1.39 +        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
    1.40 +          (app "_case_syntax"
    1.41 +            (Ast.Variable "x",
    1.42 +             foldr1 (app "_case2") (map_index (case1 authentic) spec)),
    1.43 +           capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x"))
    1.44        fun one_abscon_trans authentic (n, c) =
    1.45 -          (if authentic then Parse_Print_Rule else Parse_Rule)
    1.46 -            (cabs (con1 authentic n c, expvar n),
    1.47 -             capps (case_constant, map_index (when1 n) spec))
    1.48 +        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
    1.49 +          (cabs (con1 authentic n c, expvar n),
    1.50 +           capps (case_constant, map_index (when1 n) spec))
    1.51        fun abscon_trans authentic =
    1.52            map_index (one_abscon_trans authentic) spec
    1.53 -      val trans_rules : ast Syntax.trrule list =
    1.54 +      val trans_rules : Ast.ast Syntax.trrule list =
    1.55            case_trans false :: case_trans true ::
    1.56            abscon_trans false @ abscon_trans true
    1.57      in