src/Pure/Isar/locale.ML
changeset 12514 4bdbc5a977f6
parent 12510 172d18ec3b54
child 12529 d99716a53f59
equal deleted inserted replaced
12513:0ffb824dc95c 12514:4bdbc5a977f6
   484 
   484 
   485     val (import_ctxt, import_elemss) = declare_expr (context, import);
   485     val (import_ctxt, import_elemss) = declare_expr (context, import);
   486     val (ctxt, elemss) = apsnd flat (foldl_map declare_element (import_ctxt, elements));
   486     val (ctxt, elemss) = apsnd flat (foldl_map declare_element (import_ctxt, elements));
   487     val type_env = frozen_tvars ctxt (mapfilter (ProofContext.default_type ctxt o #1)
   487     val type_env = frozen_tvars ctxt (mapfilter (ProofContext.default_type ctxt o #1)
   488       (fixes_of_elemss import_elemss @ fixes_of_elemss elemss));
   488       (fixes_of_elemss import_elemss @ fixes_of_elemss elemss));
   489     val FIXME = PolyML.print type_env;
       
   490 
   489 
   491     fun inst_elems ((name, ps), elems) = ((name, ps), elems);    (* FIXME *)
   490     fun inst_elems ((name, ps), elems) = ((name, ps), elems);    (* FIXME *)
   492 
   491 
   493     val import_elemss' = map inst_elems import_elemss;
   492     val import_elemss' = map inst_elems import_elemss;
   494     val import_ctxt' = context |> activate_elemss import_elemss';
   493     val import_ctxt' = context |> activate_elemss import_elemss';