src/Pure/codegen.ML
changeset 24707 dfeb98f84e93
parent 24688 a5754ca5c510
child 24805 34cbfb87dfe8
     1.1 --- a/src/Pure/codegen.ML	Tue Sep 25 13:28:35 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Tue Sep 25 13:28:37 2007 +0200
     1.3 @@ -197,7 +197,7 @@
     1.4  
     1.5  fun set_default_type s thy ({size, iterations, ...} : test_params) =
     1.6    {size = size, iterations = iterations,
     1.7 -   default_type = SOME (Sign.read_typ thy s)};
     1.8 +   default_type = SOME (Syntax.read_typ_global thy s)};
     1.9  
    1.10  
    1.11  (* theory data *)
    1.12 @@ -1112,7 +1112,7 @@
    1.13      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
    1.14       (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
    1.15         (fn ((name, mfx), aux) => (name, (parse_mixfix
    1.16 -         (Sign.read_typ thy) mfx, aux)))) xs thy)));
    1.17 +         (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
    1.18  
    1.19  val assoc_constP =
    1.20    OuterSyntax.command "consts_code"
    1.21 @@ -1171,7 +1171,7 @@
    1.22  
    1.23  fun parse_tyinst xs =
    1.24    (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
    1.25 -    fn (x, ys) => (x, (v, Sign.read_typ thy s) :: ys))) xs;
    1.26 +    fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
    1.27  
    1.28  val test_paramsP =
    1.29    OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl