src/Pure/Isar/theory_target.ML
changeset 28965 1de908189869
parent 28941 128459bd72d2
child 28991 694227dd3e8c
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -59,9 +59,9 @@
     1.4    let
     1.5      val thy = ProofContext.theory_of ctxt;
     1.6      val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
     1.7 -    val fixes = map (fn (x, T) => (Name.binding x, SOME T, NoSyn))
     1.8 +    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
     1.9        (#1 (ProofContext.inferred_fixes ctxt));
    1.10 -    val assumes = map (fn A => (Attrib.no_binding, [(Thm.term_of A, [])]))
    1.11 +    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    1.12        (Assumption.assms_of ctxt);
    1.13      val elems =
    1.14        (if null fixes then [] else [Element.Fixes fixes]) @
    1.15 @@ -195,13 +195,13 @@
    1.16  
    1.17  fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
    1.18    let
    1.19 -    val b' = Morphism.name phi b;
    1.20 +    val b' = Morphism.binding phi b;
    1.21      val rhs' = Morphism.term phi rhs;
    1.22      val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
    1.23      val arg = (b', Term.close_schematic_term rhs');
    1.24      val similar_body = Type.similar_types (rhs, rhs');
    1.25      (* FIXME workaround based on educated guess *)
    1.26 -    val (prefix', _) = Binding.dest_binding b';
    1.27 +    val (prefix', _) = Binding.dest b';
    1.28      val class_global = Name.name_of b = Name.name_of b'
    1.29        andalso not (null prefix')
    1.30        andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
    1.31 @@ -292,7 +292,7 @@
    1.32      val thy_ctxt = ProofContext.init thy;
    1.33  
    1.34      val c = Name.name_of b;
    1.35 -    val name' = Name.map_name (Thm.def_name_optional c) name;
    1.36 +    val name' = Binding.map_base (Thm.def_name_optional c) name;
    1.37      val (rhs', rhs_conv) =
    1.38        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
    1.39      val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];