src/HOL/Import/hol4rews.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18921 f47c46d7d654
     1.1 --- a/src/HOL/Import/hol4rews.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -258,15 +258,16 @@
     1.4  val hol4_debug = ref false
     1.5  fun message s = if !hol4_debug then writeln s else ()
     1.6  
     1.7 -fun add_hol4_rewrite (thy,th) =
     1.8 +fun add_hol4_rewrite (context, th) =
     1.9      let
    1.10 +        val thy = Context.the_theory context;
    1.11  	val _ = message "Adding HOL4 rewrite"
    1.12  	val th1 = th RS eq_reflection
    1.13  	val current_rews = HOL4Rewrites.get thy
    1.14  	val new_rews = gen_ins Thm.eq_thm (th1,current_rews)
    1.15  	val updated_thy  = HOL4Rewrites.put new_rews thy
    1.16      in
    1.17 -	(updated_thy,th1)
    1.18 +	(Context.Theory updated_thy,th1)
    1.19      end;
    1.20  
    1.21  fun ignore_hol4 bthy bthm thy =
    1.22 @@ -775,8 +776,5 @@
    1.23    ImportSegment.init #>
    1.24    initial_maps #>
    1.25    Attrib.add_attributes
    1.26 -    [("hol4rew",
    1.27 -      (Attrib.no_args add_hol4_rewrite,
    1.28 -       Attrib.no_args Attrib.undef_local_attribute),
    1.29 -      "HOL4 rewrite rule")]
    1.30 +    [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
    1.31  end