--- a/src/HOL/TLA/Action.ML Mon Oct 20 11:14:16 1997 +0200
+++ b/src/HOL/TLA/Action.ML Mon Oct 20 11:14:55 1997 +0200
@@ -51,7 +51,7 @@
*)
fun maybe_unlift th =
(case concl_of th of
- Const("TrueInt",_) $ p
+ Const("Intensional.TrueInt",_) $ p
=> (action_unlift th
handle _ => int_unlift th)
| _ => th);
--- a/src/HOL/TLA/Intensional.ML Mon Oct 20 11:14:16 1997 +0200
+++ b/src/HOL/TLA/Intensional.ML Mon Oct 20 11:14:55 1997 +0200
@@ -86,7 +86,7 @@
*)
fun maybe_unlift th =
(case concl_of th of
- Const("TrueInt",_) $ p => int_unlift th
+ Const("Intensional.TrueInt",_) $ p => int_unlift th
| _ => th);
simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
--- a/src/HOL/TLA/ROOT.ML Mon Oct 20 11:14:16 1997 +0200
+++ b/src/HOL/TLA/ROOT.ML Mon Oct 20 11:14:55 1997 +0200
@@ -12,6 +12,8 @@
*)
Syntax.ambiguity_level := 10000;
+reset global_names;
+
use_thy "TLA";
val TLA_build_completed = ();
--- a/src/HOL/TLA/hypsubst.ML Mon Oct 20 11:14:16 1997 +0200
+++ b/src/HOL/TLA/hypsubst.ML Mon Oct 20 11:14:55 1997 +0200
@@ -88,7 +88,7 @@
Is type ty the type of a state variable? Only then do we substitute
in applications. This function either returns true or raises Match.
*)
-fun is_stvar (Type("fun", Type("state",[])::_)) = true;
+fun is_stvar (Type("fun", Type("Stfun.state",[])::_)) = true;
(*If novars then we forbid Vars in the equality.
--- a/src/HOL/add_ind_def.ML Mon Oct 20 11:14:16 1997 +0200
+++ b/src/HOL/add_ind_def.ML Mon Oct 20 11:14:55 1997 +0200
@@ -68,8 +68,9 @@
val rec_names = map (#1 o dest_Const) rec_hds
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
- val _ = assert_all Syntax.is_identifier rec_names
- (fn a => "Name of recursive set not an identifier: " ^ a);
+ val rec_base_names = map Sign.base_name rec_names;
+ val _ = assert_all Syntax.is_identifier rec_base_names
+ (fn a => "Base name of recursive set not an identifier: " ^ a);
local (*Checking the introduction rules*)
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
@@ -136,7 +137,8 @@
(*A key definition:
If no mutual recursion then it equals the one recursive set.
If mutual recursion then it differs from all the recursive sets. *)
- val big_rec_name = space_implode "_" rec_names;
+ val big_rec_base_name = space_implode "_" rec_base_names;
+ val big_rec_name = Sign.full_name sign big_rec_base_name;
(*Big_rec... is the union of the mutually recursive sets*)
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
@@ -160,86 +162,4 @@
in thy |> Theory.add_defs_i axpairs end
-(****************************************************************OMITTED
-
-(*Expects the recursive sets to have been defined already.
- con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
-fun add_constructs_def (rec_names, con_ty_lists) thy =
-* let
-* val _ = writeln" Defining the constructor functions...";
-* val case_name = "f"; (*name for case variables*)
-
-* (** Define the constructors **)
-
-* (*The empty tuple is 0*)
-* fun mk_tuple [] = Const("0",iT)
-* | mk_tuple args = foldr1 mk_Pair args;
-
-* fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k;
-
-* val npart = length rec_names; (*total # of mutually recursive parts*)
-
-* (*Make constructor definition; kpart is # of this mutually recursive part*)
-* fun mk_con_defs (kpart, con_ty_list) =
-* let val ncon = length con_ty_list (*number of constructors*)
- fun mk_def (((id,T,syn), name, args, prems), kcon) =
- (*kcon is index of constructor*)
- mk_defpair (list_comb (Const(name,T), args),
- mk_inject npart kpart
- (mk_inject ncon kcon (mk_tuple args)))
-* in ListPair.map mk_def (con_ty_list, (1 upto ncon)) end;
-
-* (** Define the case operator **)
-
-* (*Combine split terms using case; yields the case operator for one part*)
-* fun call_case case_list =
-* let fun call_f (free,args) =
- ap_split T free (map (#2 o dest_Free) args)
-* in fold_bal (app sum_case) (map call_f case_list) end;
-
-* (** Generating function variables for the case definition
- Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
-
-* (*Treatment of a single constructor*)
-* fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
- if Syntax.is_identifier id
- then (opno,
- (Free(case_name ^ "_" ^ id, T), args) :: cases)
- else (opno+1,
- (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) ::
- cases)
-
-* (*Treatment of a list of constructors, for one part*)
-* fun add_case_list (con_ty_list, (opno,case_lists)) =
- let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
- in (opno', case_list :: case_lists) end;
-
-* (*Treatment of all parts*)
-* val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
-
-* val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
-
-* val big_rec_name = space_implode "_" rec_names;
-
-* val big_case_name = big_rec_name ^ "_case";
-
-* (*The list of all the function variables*)
-* val big_case_args = flat (map (map #1) case_lists);
-
-* val big_case_tm =
- list_comb (Const(big_case_name, big_case_typ), big_case_args);
-
-* val big_case_def = mk_defpair
- (big_case_tm, fold_bal (app sum_case) (map call_case case_lists));
-
-* (** Build the new theory **)
-
-* val const_decs =
- (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
-
-* val axpairs =
- big_case_def :: flat (ListPair.map mk_con_defs ((1 upto npart), con_ty_lists))
-
-* in thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs end;
-****************************************************************)
end;
--- a/src/HOL/datatype.ML Mon Oct 20 11:14:16 1997 +0200
+++ b/src/HOL/datatype.ML Mon Oct 20 11:14:55 1997 +0200
@@ -4,8 +4,6 @@
Konrad Slind
Copyright 1995 TU Muenchen
-TODO:
- - handle internal / external names
*)
(** Information about datatypes **)
@@ -129,7 +127,7 @@
| subst (funct $ body) =
let val (f,b) = strip_comb (funct$body)
in
- if is_Const f andalso fst(dest_Const f) = fname
+ if is_Const f andalso Sign.base_name (fst(dest_Const f)) = fname
then
let val (ls,rest) = (take(rpos,b), drop(rpos,b));
val (xk,rs) = (hd rest,tl rest)
@@ -181,9 +179,9 @@
raise RecError "more than one non-variable in pattern"
else if not(null(findrep (map fst (ls @ rs @ cargs)))) then
raise RecError "repeated variable name in pattern"
- else (fst(dest_Const name) handle TERM _ =>
+ else (Sign.base_name (fst(dest_Const name)) handle TERM _ =>
raise RecError "function is not declared as constant in theory"
- ,rpos,ls,fst( dest_Const c),cargs,rs,rhs)
+ ,rpos,ls, Sign.base_name (fst(dest_Const c)),cargs,rs,rhs)
end;
(* check function specified for all constructors and sort function terms *)
@@ -506,7 +504,7 @@
Logic.mk_equals (Const(fname,dummyT), rhs))
val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
val varT = Type.varifyT T;
- val ftyp = the (Sign.const_type sg fname);
+ val ftyp = the (Sign.const_type sg (Sign.intern_const sg fname));
in Theory.add_defs_i [defpairT] thy end;
in
@@ -962,7 +960,10 @@
in
fun build_record (thy,(ty,cl),itac) =
let val sign = sign_of thy
- fun const s = Const(s, the(Sign.const_type sign s))
+ val intern_const = Sign.intern_const sign;
+ fun const s =
+ let val s' = intern_const s
+ in Const(s', the (Sign.const_type sign s')) end
val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
val {nchotomy,case_cong} = case_thms sign case_rewrites itac
val exhaustion = mk_exhaust nchotomy
--- a/src/HOL/thy_syntax.ML Mon Oct 20 11:14:16 1997 +0200
+++ b/src/HOL/thy_syntax.ML Mon Oct 20 11:14:55 1997 +0200
@@ -143,7 +143,8 @@
\ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
\end;\n\
\val dummy = datatypes := Dtype.build_record (thy, " ^
- mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^
+ mk_pair ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
+ mk_list (map (fst o fst) cons)) ^
", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
\val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
\val dummy = AddIffs " ^ tname ^ ".inject;\n\