--- 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";