src/HOL/Tools/SMT/smt_translate.ML
changeset 40161 539d07b00e5f
parent 39535 cd1bb7125d8a
child 40274 6486c610a549
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Oct 26 11:31:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Oct 26 11:39:26 2010 +0200
     1.3 @@ -43,9 +43,9 @@
     1.4      typs: typ Symtab.table,
     1.5      terms: term Symtab.table,
     1.6      unfolds: thm list,
     1.7 -    assms: thm list }
     1.8 +    assms: (int * thm) list }
     1.9  
    1.10 -  val translate: config -> Proof.context -> string list -> thm list ->
    1.11 +  val translate: config -> Proof.context -> string list -> (int * thm) list ->
    1.12      string * recon
    1.13  end
    1.14  
    1.15 @@ -101,7 +101,7 @@
    1.16    typs: typ Symtab.table,
    1.17    terms: term Symtab.table,
    1.18    unfolds: thm list,
    1.19 -  assms: thm list }
    1.20 +  assms: (int * thm) list }
    1.21  
    1.22  
    1.23  
    1.24 @@ -244,8 +244,9 @@
    1.25            else as_term (in_term t)
    1.26        | _ => as_term (in_term t))
    1.27    in
    1.28 -    map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms),
    1.29 -    map (in_form o prop_of) (term_bool :: thms)))
    1.30 +    map (apsnd (normalize ctxt)) #> (fn irules =>
    1.31 +    ((unfold_rules, (~1, term_bool') :: irules),
    1.32 +     map (in_form o prop_of o snd) ((~1, term_bool) :: irules)))
    1.33    end
    1.34  
    1.35  
    1.36 @@ -318,7 +319,7 @@
    1.37               (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs))
    1.38           end)
    1.39  
    1.40 -fun relaxed thms = (([], thms), map prop_of thms)
    1.41 +fun relaxed irules = (([], irules), map (prop_of o snd) irules)
    1.42  
    1.43  fun with_context header f (ths, ts) =
    1.44    let val (us, context) = fold_map f ts empty_context