src/Pure/Isar/specification.ML
changeset 29006 abe0f11cfa4e
parent 28965 1de908189869
child 29249 4dc278c8dc59
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  fun gen_axioms do_print prep raw_vars raw_specs thy =
     1.5    let
     1.6      val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
     1.7 -    val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars;
     1.8 +    val xs = map (fn ((b, T), _) => (Binding.base_name b, T)) vars;
     1.9  
    1.10      (*consts*)
    1.11      val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
    1.12 @@ -161,7 +161,7 @@
    1.13  
    1.14      (*axioms*)
    1.15      val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
    1.16 -        fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props))
    1.17 +        fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
    1.18          #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
    1.19      val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
    1.20        (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
    1.21 @@ -187,7 +187,7 @@
    1.22          [] => (Binding.name x, NoSyn)
    1.23        | [((b, _), mx)] =>
    1.24            let
    1.25 -            val y = Name.name_of b;
    1.26 +            val y = Binding.base_name b;
    1.27              val _ = x = y orelse
    1.28                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
    1.29                  Position.str_of (Binding.pos_of b));
    1.30 @@ -220,7 +220,7 @@
    1.31          [] => (Binding.name x, NoSyn)
    1.32        | [((b, _), mx)] =>
    1.33            let
    1.34 -            val y = Name.name_of b;
    1.35 +            val y = Binding.base_name b;
    1.36              val _ = x = y orelse
    1.37                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
    1.38                  Position.str_of (Binding.pos_of b));
    1.39 @@ -281,11 +281,11 @@
    1.40    | Element.Obtains obtains =>
    1.41        let
    1.42          val case_names = obtains |> map_index (fn (i, (b, _)) =>
    1.43 -          let val name = Name.name_of b
    1.44 +          let val name = Binding.base_name b
    1.45            in if name = "" then string_of_int (i + 1) else name end);
    1.46          val constraints = obtains |> map (fn (_, (vars, _)) =>
    1.47            Element.Constrains
    1.48 -            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
    1.49 +            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.base_name x, T) | _ => NONE)));
    1.50  
    1.51          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    1.52          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
    1.53 @@ -295,7 +295,7 @@
    1.54          fun assume_case ((name, (vars, _)), asms) ctxt' =
    1.55            let
    1.56              val bs = map fst vars;
    1.57 -            val xs = map Name.name_of bs;
    1.58 +            val xs = map Binding.base_name bs;
    1.59              val props = map fst asms;
    1.60              val (Ts, _) = ctxt'
    1.61                |> fold Variable.declare_term props