Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 12 May 2010 16:18:04 +0200
changeset 2113 af11e9fbc45a
parent 2112 7c9746795767 (current diff)
parent 2110 872187804ff5 (diff)
child 2114 3201a8c3456b
merge
--- a/Nominal-General/nominal_eqvt.ML	Wed May 12 16:11:23 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Wed May 12 16:18:04 2010 +0200
@@ -10,7 +10,7 @@
   val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
   val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
   
-  val equivariance: term list -> thm -> thm list -> Proof.context -> (string * thm list) list * local_theory
+  val equivariance: term list -> thm -> thm list -> Proof.context -> thm list * local_theory
   val equivariance_cmd: string -> Proof.context -> local_theory
 end
 
@@ -142,8 +142,9 @@
   val thm_name = Binding.qualified_name 
     (Long_Name.qualify (Long_Name.base_name name) "eqvt")
   val attr = Attrib.internal (K eqvt_add)
+  val ((_, [thm']), ctxt') =  Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
 in
-  Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
+  (thm', ctxt')
 end
 
 fun equivariance pred_trms raw_induct intrs ctxt =
nominal2