src/HOL/Tools/SMT/z3_replay_util.ML
changeset 60642 48dd1cefb4ae
parent 58776 95e58e04e534
child 60868 dd18c33c001e
     1.1 --- a/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val discharge: thm -> thm -> thm
     1.5  
     1.6    (*a faster COMP*)
     1.7 -  type compose_data
     1.8 +  type compose_data = cterm list * (cterm -> cterm list) * thm
     1.9    val precompose: (cterm -> cterm list) -> thm -> compose_data
    1.10    val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
    1.11    val compose: compose_data -> thm -> thm
    1.12 @@ -71,11 +71,12 @@
    1.13  
    1.14  fun list2 (x, y) = [x, y]
    1.15  
    1.16 -fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
    1.17 -fun precompose2 f rule = precompose (list2 o f) rule
    1.18 +fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
    1.19 +fun precompose2 f rule : compose_data = precompose (list2 o f) rule
    1.20  
    1.21  fun compose (cvs, f, rule) thm =
    1.22 -  discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
    1.23 +  discharge thm
    1.24 +    (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
    1.25  
    1.26  
    1.27  (* simpset *)