src/Pure/Thy/term_style.ML

--- a/src/Pure/Thy/term_style.ML	Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Pure/Thy/term_style.ML	Tue Aug 13 20:34:46 2013 +0200
@@ -75,27 +75,27 @@
         " in propositon: " ^ Syntax.string_of_term ctxt t)
   end);
 
-fun isub_symbols (d :: s :: ss) =
+fun sub_symbols (d :: s :: ss) =
       if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
-      then d :: "\\<^isub>" :: isub_symbols (s :: ss)
+      then d :: "\\<^sub>" :: sub_symbols (s :: ss)
       else d :: s :: ss
-  | isub_symbols cs = cs;
+  | sub_symbols cs = cs;
 
-val isub_name = implode o rev o isub_symbols o rev o Symbol.explode;
+val sub_name = implode o rev o sub_symbols o rev o Symbol.explode;
 
-fun isub_term (Free (n, T)) = Free (isub_name n, T)
-  | isub_term (Var ((n, idx), T)) =
-      if idx <> 0 then Var ((isub_name (n ^ string_of_int idx), 0), T)
-      else Var ((isub_name n, 0), T)
-  | isub_term (t $ u) = isub_term t $ isub_term u
-  | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
-  | isub_term t = t;
+fun sub_term (Free (n, T)) = Free (sub_name n, T)
+  | sub_term (Var ((n, idx), T)) =
+      if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T)
+      else Var ((sub_name n, 0), T)
+  | sub_term (t $ u) = sub_term t $ sub_term u
+  | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
+  | sub_term t = t;
 
 val _ = Context.>> (Context.map_theory
  (setup "lhs" (style_lhs_rhs fst) #>
   setup "rhs" (style_lhs_rhs snd) #>
   setup "prem" style_prem #>
   setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
-  setup "isub" (Scan.succeed (K isub_term))));
+  setup "sub" (Scan.succeed (K sub_term))));
 
 end;