src/Tools/Code/code_scala.ML
changeset 75353 05f7f5454cb6
parent 72511 460d743010bc
child 75356 fa014f31f208
equal deleted inserted replaced
75352:96c19d03b5a5 75353:05f7f5454cb6
   209             concat [print_defhead tyvars vars const vs params tys ty',
   209             concat [print_defhead tyvars vars const vs params tys ty',
   210               str ("sys.error(" ^ print_scala_string const ^ ")")]
   210               str ("sys.error(" ^ print_scala_string const ^ ")")]
   211           end
   211           end
   212       | print_def const (vs, ty) eqs =
   212       | print_def const (vs, ty) eqs =
   213           let
   213           let
   214             val tycos = fold (fn ((ts, t), _) =>
   214             val tycos = build (fold (fn ((ts, t), _) =>
   215               fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
   215               fold Code_Thingol.add_tyconames (t :: ts)) eqs);
   216             val tyvars = reserved
   216             val tyvars = reserved
   217               |> intro_base_names
   217               |> intro_base_names
   218                    (is_none o tyco_syntax) deresolve_tyco tycos
   218                    (is_none o tyco_syntax) deresolve_tyco tycos
   219               |> intro_tyvars vs;
   219               |> intro_tyvars vs;
   220             val simple = case eqs
   220             val simple = case eqs