diff -r ddd97d9dfbfb -r 74f0dcc0b5fb src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Thu Oct 29 11:41:36 2009 +0100
+++ b/src/HOL/Fact.thy	Thu Oct 29 11:41:37 2009 +0100
@@ -8,7 +8,7 @@
 header{*Factorial Function*}
 
 theory Fact
-imports Nat_Transfer
+imports Main
 begin
 
 class fact =
@@ -266,9 +266,6 @@
 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
 by auto
 
-class ordered_semiring_1 = ordered_semiring + semiring_1
-class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
-
 lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
 
 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"