src/HOL/Decision_Procs/mir_tac.ML
changeset 36945 9bec62c10714
parent 36692 54b64d4ad524
child 37887 2ae085b07f2f
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4      val pre_thm = Seq.hd (EVERY
     1.5        [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
     1.6         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac mir_ss 1)]
     1.7 -      (trivial ct))
     1.8 +      (Thm.trivial ct))
     1.9      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    1.10      (* The result of the quantifier elimination *)
    1.11      val (th, tac) = case (prop_of pre_thm) of