--- a/src/Pure/drule.ML Sun Aug 05 20:32:18 2018 +0200
+++ b/src/Pure/drule.ML Mon Aug 06 11:06:43 2018 +0200
@@ -98,8 +98,6 @@
val is_sort_constraint: term -> bool
val sort_constraintI: thm
val sort_constraint_eq: thm
- val sort_constraint_intr: indexname * sort -> thm -> thm
- val sort_constraint_intr_shyps: thm -> thm
val with_subgoal: int -> (thm -> thm) -> thm -> thm
val comp_no_flatten: thm * int -> int -> thm -> thm
val rename_bvars: (string * string) list -> thm -> thm
@@ -649,26 +647,6 @@
(Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
(implies_intr_list [A, C] (Thm.assume A)));
-val sort_constraint_eq' = Thm.symmetric sort_constraint_eq;
-
-fun sort_constraint_intr tvar thm =
- Thm.equal_elim
- (Thm.instantiate
- ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))],
- [((("A", 0), propT), Thm.cprop_of thm)])
- sort_constraint_eq') thm;
-
-fun sort_constraint_intr_shyps raw_thm =
- let val thm = Thm.strip_shyps raw_thm in
- (case Thm.extra_shyps thm of
- [] => thm
- | shyps =>
- let
- val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm []));
- val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps;
- in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end)
- end;
-
end;