src/Pure/conjunction.ML
changeset 26424 a6cad32a27b0
parent 24976 821628d16552
child 26485 b90d1fc201de
     1.1 --- a/src/Pure/conjunction.ML	Thu Mar 27 14:41:07 2008 +0100
     1.2 +++ b/src/Pure/conjunction.ML	Thu Mar 27 14:41:09 2008 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  (** abstract syntax **)
     1.6  
     1.7 -val cert = Thm.cterm_of ProtoPure.thy;
     1.8 +val cert = Thm.cterm_of (Context.the_theory (Context.the_thread_data ()));
     1.9  val read_prop = cert o SimpleSyntax.read_prop;
    1.10  
    1.11  val true_prop = cert Logic.true_prop;
    1.12 @@ -42,7 +42,7 @@
    1.13  
    1.14  fun dest_conjunction ct =
    1.15    (case Thm.term_of ct of
    1.16 -    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    1.17 +    (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    1.18    | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
    1.19  
    1.20  
    1.21 @@ -69,7 +69,8 @@
    1.22  val ABC = read_prop "A ==> B ==> C";
    1.23  val A_B = read_prop "A && B";
    1.24  
    1.25 -val conjunction_def = Thm.unvarify ProtoPure.conjunction_def;
    1.26 +val conjunction_def =
    1.27 +  Thm.unvarify (Thm.get_axiom (Context.the_theory (Context.the_thread_data ())) "conjunction_def");
    1.28  
    1.29  fun conjunctionD which =
    1.30    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
    1.31 @@ -121,8 +122,8 @@
    1.32  
    1.33  local
    1.34  
    1.35 -fun conjs n =
    1.36 -  let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
    1.37 +fun conjs thy n =
    1.38 +  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
    1.39    in (As, mk_conjunction_balanced As) end;
    1.40  
    1.41  val B = read_prop "B";
    1.42 @@ -142,7 +143,8 @@
    1.43    if n < 2 then th
    1.44    else
    1.45      let
    1.46 -      val (As, C) = conjs n;
    1.47 +      val thy = Thm.theory_of_thm th;
    1.48 +      val (As, C) = conjs thy n;
    1.49        val D = Drule.mk_implies (C, B);
    1.50      in
    1.51        comp_rule th
    1.52 @@ -159,7 +161,8 @@
    1.53    if n < 2 then th
    1.54    else
    1.55      let
    1.56 -      val (As, C) = conjs n;
    1.57 +      val thy = Thm.theory_of_thm th;
    1.58 +      val (As, C) = conjs thy n;
    1.59        val D = Drule.list_implies (As, B);
    1.60      in
    1.61        comp_rule th