src/Pure/Isar/proof_context.ML
changeset 19274 b85e16bd70d0
parent 19270 d928b5468c43
child 19310 9b2080d9ed28
equal deleted inserted replaced
19273:05b6d220e509 19274:b85e16bd70d0
   660 fun rename_frees ctxt ts frees =
   660 fun rename_frees ctxt ts frees =
   661   let
   661   let
   662     val (types, sorts, _, _) = defaults_of (ctxt |> fold declare_syntax ts);
   662     val (types, sorts, _, _) = defaults_of (ctxt |> fold declare_syntax ts);
   663     fun rename (x, X) xs =
   663     fun rename (x, X) xs =
   664       let
   664       let
   665         fun used y = member (op =) xs y orelse
   665         fun used y = y = "" orelse y = "'" orelse member (op =) xs y orelse
   666           Vartab.defined types (y, ~1) orelse Vartab.defined sorts (y, ~1);
   666           Vartab.defined types (y, ~1) orelse Vartab.defined sorts (y, ~1);
   667         val x' = Term.variant_name used x;
   667         val x' = Term.variant_name used x;
   668       in ((x', X), x' :: xs) end;
   668       in ((x', X), x' :: xs) end;
   669   in #1 (fold_map rename frees []) end;
   669   in #1 (fold_map rename frees []) end;
   670 
   670 
   723 (* polymorphic terms *)
   723 (* polymorphic terms *)
   724 
   724 
   725 fun monomorphic ctxt ts =
   725 fun monomorphic ctxt ts =
   726   let
   726   let
   727     val tvars = fold Term.add_tvars ts [];
   727     val tvars = fold Term.add_tvars ts [];
   728     val tfrees = map TFree (rename_frees ctxt ts (map (apfst fst) tvars));
   728     val tfrees = map TFree (rename_frees ctxt ts (map (pair "'" o #2) tvars));
   729     val specialize = Term.instantiate ((tvars ~~ tfrees), []);
   729     val specialize = Term.instantiate ((tvars ~~ tfrees), []);
   730   in map specialize ts end;
   730   in map specialize ts end;
   731 
   731 
   732 fun polymorphic ctxt ts =
   732 fun polymorphic ctxt ts =
   733   generalize (ctxt |> fold declare_term ts) ctxt ts;
   733   generalize (ctxt |> fold declare_term ts) ctxt ts;