# HG changeset patch
# User haftmann
# Date 1281361887 -7200
# Node ID 4647c2c81d74afc934fac2d9a5da3509319aaa0d
# Parent  502251f34bdc49e097ea1a1ad12211f37470e0ac
more appropriate outline of `define`

diff -r 502251f34bdc -r 4647c2c81d74 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Aug 09 15:43:37 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Aug 09 15:51:27 2010 +0200
@@ -307,7 +307,6 @@
     val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
     val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
 
-    (*const*)
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
     val term_params =
       rev (Variable.fixes_of (Local_Theory.target_of lthy))
@@ -318,8 +317,9 @@
     val params = type_params @ term_params;
 
     val U = map Term.fastype_of params ---> T;
+
+    (*foundation*)
     val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
-
     val (const, lthy2) = lthy |>
       (case Class_Target.instantiation_param lthy b of
         SOME c' =>
@@ -342,7 +342,6 @@
     val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
     val Const (head, _) = Term.head_of lhs';
 
-    (*def*)
     val (global_def, lthy4) = lthy3
       |> Local_Theory.theory_result
         (case Overloading.operation lthy b of
@@ -351,6 +350,8 @@
             if is_some (Class_Target.instantiation_param lthy b)
             then AxClass.define_overloaded name' (head, rhs')
             else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) #>> snd);
+
+    (*local definition*)
     val def = Local_Defs.trans_terms lthy4
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,