# HG changeset patch
# User wenzelm
# Date 1258376011 -3600
# Node ID 5249bbca5fab28d58959f66f6750a667dba5ba1a
# Parent  cffc97238102d1430dc6f93fd670751c3e745b11
eliminated obsolete thm position stuff;

diff -r cffc97238102 -r 5249bbca5fab src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Nov 16 13:53:02 2009 +0100
+++ b/src/Pure/more_thm.ML	Mon Nov 16 13:53:31 2009 +0100
@@ -75,9 +75,6 @@
   val untag_rule: string -> thm -> thm
   val tag: Properties.property -> attribute
   val untag: string -> attribute
-  val position_of: thm -> Position.T
-  val default_position: Position.T -> thm -> thm
-  val default_position_of: thm -> thm -> thm
   val def_name: string -> string
   val def_name_optional: string -> string -> string
   val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
@@ -380,14 +377,6 @@
 fun untag s x = rule_attribute (K (untag_rule s)) x;
 
 
-(* position *)
-
-val position_of = Position.of_properties o Thm.get_tags;
-
-fun default_position pos = Thm.map_tags (Position.default_properties pos);
-val default_position_of = default_position o position_of;
-
-
 (* def_name *)
 
 fun def_name c = c ^ "_def";