# HG changeset patch
# User wenzelm
# Date 1268509452 -3600
# Node ID 086504a943afeba89af2ca4aa9411da36986233f
# Parent  eafaa999071260ea3f4cb6ecd52288322eac124a
removed unused Args.maxidx_values and Element.generalize_facts;

diff -r eafaa9990712 -r 086504a943af src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat Mar 13 20:34:22 2010 +0100
+++ b/src/Pure/Isar/args.ML	Sat Mar 13 20:44:12 2010 +0100
@@ -14,7 +14,6 @@
   val pretty_src: Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
   val morph_values: morphism -> src -> src
-  val maxidx_values: src -> int -> int
   val assignable: src -> src
   val closure: src -> src
   val context: Proof.context context_parser
@@ -111,13 +110,6 @@
     | T.Fact ths => T.Fact (Morphism.fact phi ths)
     | T.Attribute att => T.Attribute (Morphism.transform phi att)));
 
-fun maxidx_values (Src ((_, args), _)) = args |> fold (fn arg =>
-  (case T.get_value arg of
-    SOME (T.Typ T) => Term.maxidx_typ T
-  | SOME (T.Term t) => Term.maxidx_term t
-  | SOME (T.Fact ths) => fold Thm.maxidx_thm ths
-  | _ => I));
-
 val assignable = map_args T.assignable;
 val closure = map_args T.closure;
 
diff -r eafaa9990712 -r 086504a943af src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Mar 13 20:34:22 2010 +0100
+++ b/src/Pure/Isar/element.ML	Sat Mar 13 20:44:12 2010 +0100
@@ -55,9 +55,6 @@
   val satisfy_facts: witness list ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     (Attrib.binding * (thm list * Attrib.src list) list) list
-  val generalize_facts: Proof.context -> Proof.context ->
-    (Attrib.binding * (thm list * Attrib.src list) list) list ->
-    (Attrib.binding * (thm list * Attrib.src list) list) list
   val eq_morphism: theory -> thm list -> morphism
   val transfer_morphism: theory -> morphism
   val init: context_i -> Context.generic -> Context.generic
@@ -458,22 +455,6 @@
   fact = map (MetaSimplifier.rewrite_rule thms)};
 
 
-(* generalize type/term parameters *)
-
-val maxidx_atts = fold Args.maxidx_values;
-
-fun generalize_facts inner outer facts =
-  let
-    val thy = ProofContext.theory_of inner;
-    val maxidx =
-      fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1;
-    val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer;
-    val exp_term = Drule.term_rule thy (singleton exp_fact);
-    val exp_typ = Logic.type_map exp_term;
-    val morphism = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
-  in facts_map (morph_ctxt morphism) facts end;
-
-
 (* transfer to theory using closure *)
 
 fun transfer_morphism thy =