# HG changeset patch
# User berghofe
# Date 1035213089 -7200
# Node ID 8c09e1fa24a7bb89c4ed759873652bbfb3527633
# Parent  1f8ddc4b371e1c153b4a6756aec97e8a414285a8
Removed flexpair_def.

diff -r 1f8ddc4b371e -r 8c09e1fa24a7 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Oct 21 17:11:06 2002 +0200
+++ b/src/Pure/pure_thy.ML	Mon Oct 21 17:11:29 2002 +0200
@@ -17,7 +17,6 @@
   structure ProtoPure:
     sig
       val thy: theory
-      val flexpair_def: thm
       val Goal_def: thm
     end
 end;
@@ -538,7 +537,6 @@
     (Term.dummy_patternN, "aprop", Delimfix "'_")]
   |> Theory.add_consts
    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
-    ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
     ("Goal", "prop => prop", NoSyn),
@@ -549,8 +547,6 @@
   |> Theory.add_trfuns Syntax.pure_trfuns
   |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> local_path
-  |> (#1 oo (add_defs false o map Thm.no_attributes))
-   [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
   |> (#1 oo (add_defs_i false o map Thm.no_attributes))
    [("Goal_def", let val A = Free ("A", propT) in Logic.mk_equals (Logic.mk_goal A, A) end)]
   |> (#1 o add_thmss [(("nothing", []), [])])
@@ -560,7 +556,6 @@
 structure ProtoPure =
 struct
   val thy = proto_pure;
-  val flexpair_def = get_axiom thy "flexpair_def";
   val Goal_def = get_axiom thy "Goal_def";
 end;