proper types for user-defined syntax
authorhaftmann
Fri Jan 08 14:34:18 2010 +0100 (2010-01-08)
changeset 34308394fc3cce915
parent 34307 9074aa7d06e0
child 34309 d91c3fce478e
proper types for user-defined syntax
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_scala.ML	Fri Jan 08 14:34:18 2010 +0100
     1.2 +++ b/src/Tools/Code/code_scala.ML	Fri Jan 08 14:34:18 2010 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4                  then print_case tyvars thm vars fxy cases
     1.5                  else print_app tyvars is_pat thm vars fxy c_ts
     1.6              | NONE => print_case tyvars thm vars fxy cases)
     1.7 -    and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), _)), ts)) =
     1.8 +    and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
     1.9        let
    1.10          val k = length ts;
    1.11          val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
    1.12 @@ -71,7 +71,7 @@
    1.13                (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
    1.14                  (map (print_term tyvars is_pat thm vars NOBR) ts))
    1.15            | SOME (_, print) => (false, fn ts =>
    1.16 -              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k tys));
    1.17 +              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k tys_args));
    1.18        in if k = l then print' ts
    1.19        else if k < l then
    1.20          print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)