src/HOL/Tools/set_comprehension_pointfree.ML
changeset 60781 2da59cdf531c
parent 60696 8304fb4fb823
child 61125 4c68426800de
     1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -495,9 +495,9 @@
     1.4  fun instantiate_arg_cong ctxt pred =
     1.5    let
     1.6      val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
     1.7 -    val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong)))
     1.8 +    val (Var (f, _) $ _, _) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong))
     1.9    in
    1.10 -    cterm_instantiate [(Thm.cterm_of ctxt f, Thm.cterm_of ctxt pred)] arg_cong
    1.11 +    infer_instantiate ctxt [(f, Thm.cterm_of ctxt pred)] arg_cong
    1.12    end;
    1.13  
    1.14  fun simproc ctxt redex =