src/Pure/Isar/locale.ML
changeset 14695 9c78044b99c3
parent 14643 130076a81b84
child 14777 5bb4bbdb6529
equal deleted inserted replaced
14694:49873d345a39 14695:9c78044b99c3
   474 
   474 
   475 fun frozen_tvars ctxt Ts =
   475 fun frozen_tvars ctxt Ts =
   476   let
   476   let
   477     val tvars = rev (foldl Term.add_tvarsT ([], Ts));
   477     val tvars = rev (foldl Term.add_tvarsT ([], Ts));
   478     val tfrees = map TFree
   478     val tfrees = map TFree
   479       (Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars);
   479       (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
   480   in map #1 tvars ~~ tfrees end;
   480   in map #1 tvars ~~ tfrees end;
   481 
   481 
   482 fun unify_frozen ctxt maxidx Ts Us =
   482 fun unify_frozen ctxt maxidx Ts Us =
   483   let
   483   let
   484     fun paramify (i, None) = (i, None)
   484     fun paramify (i, None) = (i, None)