# HG changeset patch
# User wenzelm
# Date 1516820913 -3600
# Node ID 182a18af5b41b9e8a8e070f67a624f856a20ab25
# Parent  dfde99d59f6e05ed9f57cb9999997e4d6c890333
tuned signature: removed unused operations;

diff -r dfde99d59f6e -r 182a18af5b41 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Jan 24 19:50:00 2018 +0100
+++ b/src/Pure/Isar/token.ML	Wed Jan 24 20:08:33 2018 +0100
@@ -82,13 +82,6 @@
   val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a
   val pretty_src: Proof.context -> src -> Pretty.T
   val ident_or_symbolic: string -> bool
-  val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
-  val source: Keyword.keywords ->
-    Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
-      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
-  val source_strict: Keyword.keywords ->
-    Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
-      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   val read_cartouche: Symbol_Pos.T list -> T
   val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list
   val explode: Keyword.keywords -> Position.T -> string -> T list
@@ -606,8 +599,6 @@
 
 (** token sources **)
 
-fun source_proper src = src |> Source.filter is_proper;
-
 local
 
 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
@@ -656,12 +647,6 @@
     val scan = if strict then scan_strict else Scan.recover scan_strict recover;
   in Source.source Symbol_Pos.stopper scan end;
 
-fun source keywords pos src =
-  Symbol_Pos.source pos src |> make_source keywords {strict = false};
-
-fun source_strict keywords pos src =
-  Symbol_Pos.source pos src |> make_source keywords {strict = true};
-
 fun read_cartouche syms =
   (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of
     SOME tok => tok
@@ -727,7 +712,7 @@
 fun read_no_commands keywords scan syms =
   Source.of_list syms
   |> make_source (Keyword.no_command_keywords keywords) {strict = true}
-  |> source_proper
+  |> Source.filter is_proper
   |> Source.source stopper (Scan.error (Scan.bulk scan))
   |> Source.exhaust;