src/Provers/splitter.ML
changeset 60781 2da59cdf531c
parent 60362 befdc10ebb42
child 62870 cf724647f75b
     1.1 --- a/src/Provers/splitter.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/Provers/splitter.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -317,9 +317,10 @@
     1.4      val (cntxt, u) = mk_cntxt t pos (T --> U);
     1.5      val trlift' = Thm.lift_rule (Thm.cprem_of state i)
     1.6        (Thm.rename_boundvars abs_lift u trlift);
     1.7 -    val (P, _) = strip_comb (fst (Logic.dest_equals
     1.8 -      (Logic.strip_assums_concl (Thm.prop_of trlift'))));
     1.9 -  in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] trlift' end;
    1.10 +    val (Var (P, _), _) =
    1.11 +      strip_comb (fst (Logic.dest_equals
    1.12 +        (Logic.strip_assums_concl (Thm.prop_of trlift'))));
    1.13 +  in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] trlift' end;
    1.14  
    1.15  
    1.16  (*************************************************************
    1.17 @@ -338,10 +339,11 @@
    1.18  fun inst_split ctxt Ts t tt thm TB state i =
    1.19    let
    1.20      val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
    1.21 -    val (P, _) = strip_comb (fst (Logic.dest_equals
    1.22 -      (Logic.strip_assums_concl (Thm.prop_of thm'))));
    1.23 +    val (Var (P, _), _) =
    1.24 +      strip_comb (fst (Logic.dest_equals
    1.25 +        (Logic.strip_assums_concl (Thm.prop_of thm'))));
    1.26      val cntxt = mk_cntxt_splitthm t tt TB;
    1.27 -  in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] thm' end;
    1.28 +  in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] thm' end;
    1.29  
    1.30  
    1.31  (*****************************************************************************