1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Tue Feb 14 19:51:39 2012 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Tue Feb 14 20:08:59 2012 +0100
     1.3 @@ -344,6 +344,7 @@
     1.4  
     1.5  
     1.6  fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
     1.7 +  (* FIXME proper use of facts!? *)
     1.8    (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
     1.9    let
    1.10      val (ctxt', _, cases, concl) = dest_hhf ctxt t