src/Pure/drule.ML
changeset 12126 34f72eb7d2db
parent 12092 d1896409ff13
child 12135 e370e5d469c2
     1.1 --- a/src/Pure/drule.ML	Fri Nov 09 10:25:10 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Nov 09 10:26:16 2001 +0100
     1.3 @@ -522,17 +522,17 @@
     1.4  
     1.5  val reflexive_thm =
     1.6    let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
     1.7 -  in store_standard_thm "reflexive" (Thm.reflexive cx) end;
     1.8 +  in open_store_standard_thm "reflexive" (Thm.reflexive cx) end;
     1.9  
    1.10  val symmetric_thm =
    1.11    let val xy = read_prop "x::'a::logic == y"
    1.12 -  in store_standard_thm "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
    1.13 +  in open_store_standard_thm "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
    1.14  
    1.15  val transitive_thm =
    1.16    let val xy = read_prop "x::'a::logic == y"
    1.17        val yz = read_prop "y::'a::logic == z"
    1.18        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    1.19 -  in store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.20 +  in open_store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.21  
    1.22  fun symmetric_fun thm = thm RS symmetric_thm;
    1.23