# HG changeset patch
# User wenzelm
# Date 774178704 -7200
# Node ID fdacecc688a149fb109f1cc63b5e353b353a8c76
# Parent  bbaa2a02bd82b03fe6e3a14507578f92e58ec5a4
minor internal renamings;

diff -r bbaa2a02bd82 -r fdacecc688a1 src/Pure/Syntax/sextension.ML
--- a/src/Pure/Syntax/sextension.ML	Thu Jul 14 11:37:08 1994 +0200
+++ b/src/Pure/Syntax/sextension.ML	Thu Jul 14 11:38:24 1994 +0200
@@ -216,9 +216,9 @@
 fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop"
   | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts;
 
-fun insort_tr (*"_insort"*) [ty, srt] =
-      srt $ (const constrainC $ const "TYPE" $ (const "itself" $ ty))
-  | insort_tr (*"_insort"*) ts = raise_term "insort_tr" ts;
+fun ofclass_tr (*"_ofclass"*) [ty, cls] =
+      cls $ (const constrainC $ const "TYPE" $ (const "itself" $ ty))
+  | ofclass_tr (*"_ofclass"*) ts = raise_term "ofclass_tr" ts;
 
 
 (* meta implication *)
@@ -358,7 +358,7 @@
       | tr' tys (Abs (x, ty, t)) = Abs (x, ty, tr' (ty :: tys) t)
       | tr' tys (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [ty])))) =
           if is_prop tys t then
-            const "_insort" $ term_of_typ show_sorts ty $ tr' tys t1
+            const "_ofclass" $ term_of_typ show_sorts ty $ tr' tys t1
           else tr' tys t1 $ tr' tys t2
       | tr' tys (t as t1 $ t2) =
           (if is_Const (head_of t) orelse not (is_prop tys t)
@@ -539,8 +539,8 @@
 val pure_trfuns =
  ([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
     ("_bigimpl", bigimpl_ast_tr)],
-  [("_abs", abs_tr), ("_aprop", aprop_tr), ("_insort", insort_tr), ("_K", k_tr),
-    ("_explode", explode_tr)],
+  [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
+    ("_K", k_tr), ("_explode", explode_tr)],
   [],
   [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr'),
     ("_implode", implode_ast_tr')]);