# HG changeset patch
# User wenzelm
# Date 1390402991 -3600
# Node ID 5792f5106c4042cfe67fab9239fc7a586c715e13
# Parent  917e799f19da8e94f525b41357977f4808ecd962
tuned signature;

diff -r 917e799f19da -r 5792f5106c40 src/Doc/ProgProve/LaTeXsugar.thy
--- a/src/Doc/ProgProve/LaTeXsugar.thy	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy	Wed Jan 22 16:03:11 2014 +0100
@@ -52,7 +52,7 @@
       end
   in
     Thy_Output.antiquotation @{binding "const_typ"}
-     (Scan.lift Args.name_source)
+     (Scan.lift Args.name_inner_syntax)
        (fn {source = src, context = ctxt, ...} => fn arg =>
           Thy_Output.output ctxt
             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
diff -r 917e799f19da -r 5792f5106c40 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/FOL/FOL.thy	Wed Jan 22 16:03:11 2014 +0100
@@ -72,7 +72,7 @@
 *}
 
 method_setup case_tac = {*
-  Args.goal_spec -- Scan.lift Args.name_source >>
+  Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
     (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
 *} "case_tac emulation (dynamic instantiation!)"
 
diff -r 917e799f19da -r 5792f5106c40 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Wed Jan 22 16:03:11 2014 +0100
@@ -106,7 +106,7 @@
       end
   in
     Thy_Output.antiquotation @{binding "const_typ"}
-     (Scan.lift Args.name_source)
+     (Scan.lift Args.name_inner_syntax)
        (fn {source = src, context = ctxt, ...} => fn arg =>
           Thy_Output.output ctxt
             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
diff -r 917e799f19da -r 5792f5106c40 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -591,7 +591,7 @@
 
 val ind_cases_setup =
   Method.setup @{binding ind_cases}
-    (Scan.lift (Scan.repeat1 Args.name_source --
+    (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
       Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
       (fn (raw_props, fixes) => fn ctxt =>
         let
diff -r 917e799f19da -r 5792f5106c40 src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy	Wed Jan 22 16:03:11 2014 +0100
@@ -16,7 +16,7 @@
     "for proving safety properties"
 
 method_setup ensures_tac = {*
-  Args.goal_spec -- Scan.lift Args.name_source >>
+  Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 *} "for proving progress properties"
 
diff -r 917e799f19da -r 5792f5106c40 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Isar/args.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -29,9 +29,9 @@
   val bracks: 'a parser -> 'a parser
   val mode: string -> bool parser
   val maybe: 'a parser -> 'a option parser
-  val cartouche_source: string parser
+  val cartouche_inner_syntax: string parser
   val cartouche_source_position: (Symbol_Pos.text * Position.T) parser
-  val name_source: string parser
+  val name_inner_syntax: string parser
   val name_source_position: (Symbol_Pos.text * Position.T) parser
   val name: string parser
   val binding: binding parser
@@ -151,10 +151,10 @@
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
 val cartouche = token Parse.cartouche;
-val cartouche_source = cartouche >> Token.source_of;
+val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
 val cartouche_source_position = cartouche >> Token.source_position_of;
 
-val name_source = named >> Token.source_of;
+val name_inner_syntax = named >> Token.inner_syntax_of;
 val name_source_position = named >> Token.source_position_of;
 
 val name = named >> Token.content_of;
@@ -182,11 +182,11 @@
 val internal_attribute = value (fn Token.Attribute att => att);
 
 fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
-fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
-fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
+fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
+fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
 
 fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
-  alt_string >> evaluate Token.Fact (get o Token.source_of);
+  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
 
 fun named_attribute att =
   internal_attribute ||
diff -r 917e799f19da -r 5792f5106c40 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Isar/parse.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -167,7 +167,7 @@
 
 fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
 fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
-fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
+fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
 
 fun kind k =
   group (fn () => Token.str_of_kind k)
diff -r 917e799f19da -r 5792f5106c40 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -41,7 +41,7 @@
   val is_space: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
-  val source_of: T -> string
+  val inner_syntax_of: T -> string
   val source_position_of: T -> Symbol_Pos.text * Position.T
   val content_of: T -> string
   val unparse: T -> string
@@ -206,7 +206,7 @@
 
 (* token content *)
 
-fun source_of (Token ((source, (pos, _)), (_, x), _)) =
+fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) =
   if YXML.detect x then x
   else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
 
diff -r 917e799f19da -r 5792f5106c40 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -99,14 +99,14 @@
 
   value (Binding.name "cpat")
     (Args.context --
-      Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
+      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
         "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
           ML_Syntax.atomic (ML_Syntax.print_term t))));
 
 
 (* type classes *)
 
-fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   Proof_Context.read_class ctxt s
   |> syn ? Lexicon.mark_class
   |> ML_Syntax.print_string);
@@ -116,13 +116,13 @@
   inline (Binding.name "class_syntax") (class true) #>
 
   inline (Binding.name "sort")
-    (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
       ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
 
 
 (* type constructors *)
 
-fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
+fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
       val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
@@ -146,7 +146,7 @@
 
 (* constants *)
 
-fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
+fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
       val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
@@ -169,7 +169,7 @@
       else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
 
   inline (Binding.name "const")
-    (Args.context -- Scan.lift Args.name_source -- Scan.optional
+    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
       >> (fn ((ctxt, raw_c), Ts) =>
         let
diff -r 917e799f19da -r 5792f5106c40 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -85,7 +85,7 @@
 
 val and_ = Args.$$$ "and";
 val by = Args.$$$ "by";
-val goal = Scan.unless (by || and_) Args.name_source;
+val goal = Scan.unless (by || and_) Args.name_inner_syntax;
 
 val _ = Theory.setup
   (ML_Context.add_antiq (Binding.name "lemma")
diff -r 917e799f19da -r 5792f5106c40 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -570,9 +570,9 @@
   basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
   basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
   basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
-  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
+  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
   basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
-  basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
+  basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
   basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
   basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
   basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
diff -r 917e799f19da -r 5792f5106c40 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -165,7 +165,7 @@
 
 val _ = Theory.setup
   (Attrib.setup @{binding "where"}
-    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
+    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >>
       (fn args =>
         Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
     "named instantiation of theorem");
@@ -175,7 +175,7 @@
 
 local
 
-val inst = Args.maybe Args.name_source;
+val inst = Args.maybe Args.name_inner_syntax;
 val concl = Args.$$$ "concl" -- Args.colon;
 
 val insts =
@@ -320,7 +320,7 @@
 fun method inst_tac tac =
   Args.goal_spec --
   Scan.optional (Scan.lift
-    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
+    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --|
       Args.$$$ "in")) [] --
   Attrib.thms >>
   (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
@@ -347,12 +347,12 @@
   Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
     "cut rule (dynamic instantiation)" #>
   Method.setup @{binding subgoal_tac}
-    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
+    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
       (fn (quant, props) => fn ctxt =>
         SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
     "insert subgoal (dynamic instantiation)" #>
   Method.setup @{binding thin_tac}
-    (Args.goal_spec -- Scan.lift Args.name_source >>
+    (Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
       (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
       "remove premise (dynamic instantiation)");
 
diff -r 917e799f19da -r 5792f5106c40 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Tools/induct_tacs.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -122,13 +122,14 @@
 val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
 
 val varss =
-  Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
+  Parse.and_list'
+    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax))));
 
 in
 
 val setup =
   Method.setup @{binding case_tac}
-    (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
+    (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
       (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
     "unstructured case analysis on types" #>
   Method.setup @{binding induct_tac}
diff -r 917e799f19da -r 5792f5106c40 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -57,7 +57,7 @@
 
 val setup =
   Method.setup @{binding "ind_cases"}
-    (Scan.lift (Scan.repeat1 Args.name_source) >>
+    (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
       (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
     "dynamic case analysis on sets";
 
diff -r 917e799f19da -r 5792f5106c40 src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Wed Jan 22 16:03:11 2014 +0100
@@ -375,7 +375,7 @@
 *}
 
 method_setup ensures = {*
-    Args.goal_spec -- Scan.lift Args.name_source >>
+    Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
     (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 *} "for proving progress properties"