tuned;
authorwenzelm
Sun Nov 15 15:14:28 2009 +0100 (2009-11-15)
changeset 336977d6793ce0a26
parent 33696 2c7c79ca6c23
child 33698 b5f36fa5a7b4
tuned;
src/HOL/Tools/Function/induction_schema.ML
src/Pure/more_thm.ML
src/Pure/term.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 15 15:14:02 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 15 15:14:28 2009 +0100
     1.3 @@ -383,7 +383,7 @@
     1.4  
     1.5      val res = Conjunction.intr_balanced (map_index project branches)
     1.6                   |> fold_rev implies_intr (map cprop_of newgoals @ steps)
     1.7 -                 |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm)
     1.8 +                 |> Drule.generalize ([], [Rn])
     1.9  
    1.10      val nbranches = length branches
    1.11      val npres = length pres
     2.1 --- a/src/Pure/more_thm.ML	Sun Nov 15 15:14:02 2009 +0100
     2.2 +++ b/src/Pure/more_thm.ML	Sun Nov 15 15:14:28 2009 +0100
     2.3 @@ -279,9 +279,10 @@
     2.4  
     2.5  val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars;
     2.6  
     2.7 -fun forall_elim_var i th = forall_elim_vars_aux
     2.8 -  (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
     2.9 -  | _ => raise THM ("forall_elim_vars", i, [th])) i th;
    2.10 +fun forall_elim_var i th =
    2.11 +  forall_elim_vars_aux
    2.12 +    (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
    2.13 +      | _ => raise THM ("forall_elim_vars", i, [th])) i th;
    2.14  
    2.15  end;
    2.16  
     3.1 --- a/src/Pure/term.ML	Sun Nov 15 15:14:02 2009 +0100
     3.2 +++ b/src/Pure/term.ML	Sun Nov 15 15:14:28 2009 +0100
     3.3 @@ -467,7 +467,7 @@
     3.4  val add_tvars = fold_types add_tvarsT;
     3.5  val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
     3.6  val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
     3.7 -val add_tfree_namesT = fold_atyps (fn TFree (xi, _) => insert (op =) xi | _ => I);
     3.8 +val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
     3.9  val add_tfree_names = fold_types add_tfree_namesT;
    3.10  val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
    3.11  val add_tfrees = fold_types add_tfreesT;
     4.1 --- a/src/Pure/thm.ML	Sun Nov 15 15:14:02 2009 +0100
     4.2 +++ b/src/Pure/thm.ML	Sun Nov 15 15:14:28 2009 +0100
     4.3 @@ -1068,8 +1068,9 @@
     4.4          val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = th;
     4.5          val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
     4.6  
     4.7 -        val bad_type = if null tfrees then K false else
     4.8 -          Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false);
     4.9 +        val bad_type =
    4.10 +          if null tfrees then K false
    4.11 +          else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false);
    4.12          fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x
    4.13            | bad_term (Var (_, T)) = bad_type T
    4.14            | bad_term (Const (_, T)) = bad_type T