src/HOL/Import/shuffler.ML
changeset 20897 3f8d2834b2c4
parent 20854 f9cf9e62d11c
child 20951 868120282837
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat Oct 07 07:41:56 2006 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Mon Oct 09 02:19:49 2006 +0200
     1.3 @@ -681,7 +681,7 @@
     1.4  	else ShuffleData.put (thm::shuffles) thy
     1.5      end
     1.6  
     1.7 -val shuffle_attr = Thm.declaration_attribute (Context.map_theory o add_shuffle_rule);
     1.8 +val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
     1.9  
    1.10  val setup =
    1.11    Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>