src/HOL/Tools/Function/induction_schema.ML
changeset 42495 1af81b70cf09
parent 42361 23f352990944
child 46217 7b19666f0e3d
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 27 20:58:40 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 27 21:50:04 2011 +0200
     1.3 @@ -55,9 +55,9 @@
     1.4  
     1.5  fun dest_hhf ctxt t =
     1.6    let
     1.7 -    val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
     1.8 +    val ((params, imp), ctxt') = Variable.focus t ctxt
     1.9    in
    1.10 -    (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    1.11 +    (ctxt', map #2 params, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    1.12    end
    1.13  
    1.14  fun mk_scheme' ctxt cases concl =