eliminated obsolete thm position stuff;
authorwenzelm
Mon, 16 Nov 2009 13:53:31 +0100
changeset 33713 5249bbca5fab
parent 33712 cffc97238102
child 33720 d15212c7501c
eliminated obsolete thm position stuff;
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";