src/HOL/Tools/Function/induction_schema.ML
changeset 41117 d6379876ec4c
parent 39756 6c8e83d94536
child 41225 bd4ecd48c21f
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Mon Dec 13 10:15:26 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Dec 13 10:15:27 2010 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  
     1.5  fun dest_hhf ctxt t =
     1.6    let
     1.7 -    val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
     1.8 +    val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
     1.9    in
    1.10      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    1.11    end